hopv/hoice

Issues

• "invalid datatype declaration, unknown sort" when using testers

  #73 opened 3 months ago by coord-e
  0

• hoice get stuck during preprocessing

  #67 opened 9 months ago by naokikob
  1

• hoice crush with "-v -v -v"

  #69 opened a year ago by naokikob
  0

• Error for unsat proof

  #65 opened a year ago by izumitanaka
  2

• Stack overflow

  #63 opened a year ago by naokikob
  2

• Too slow to parse

  #62 opened 2 years ago by ryosu-sato
  1

• cargo test fails in rust 1.64.0

  #59 opened 2 years ago by moratorium08
  1

• Release-built hoice sometimes crashes while learning on macOS Monterey

  #57 opened 3 years ago by khei4
  7

• bug?

  #55 opened 4 years ago by naokikob
  1

• bug: "invalid named expression"?

  #54 opened 4 years ago by naokikob
  1

• parse error on CHCs with ground assertions

  #52 opened 4 years ago by hgvk94
  1

• Parse error for sorts beginning with Int

  #50 opened 4 years ago by shiatsumat
  1

• Mysterious bug on lists and pairs

  #36 opened 5 years ago by shiatsumat
  3

• Fix/Enhance Error-Handling

  #49 opened 4 years ago by AdrienChampion
  0

• Hoice fails to generate unsat proof when the backend z3 version is 4.8.8

  #37 opened 5 years ago by moratorium08
  5

• Mysterious bug around conditional branching

  #46 opened 4 years ago by shiatsumat
  2

• Parsing or

  #40 opened 4 years ago by naokikob
  1

• a fresh declaration was already defined under Z3 4.8.9

  #41 opened 4 years ago by shosy
  2

• Failed to parse model from solver.

  #45 opened 4 years ago by gyggg
  2

• Parse error on result of `get-model` for Z3

  #43 opened 4 years ago by gyggg
  2

• Bug?

  #29 opened 6 years ago by naokikob
  2

• Bug?

  #28 opened 6 years ago by naokikob
  2

• Another bug?

  #30 opened 6 years ago by naokikob
  0

• How SVCOMP benchmark programs are converting to Ocamal programs or to Horn cluases

  #19 opened 7 years ago by ezudheen
  7