handle unit type in z3 solver, and parse function with unit return type....
handle unit type in z3 solver, and parse function with unit return type. Disable UnitEliminationPass
Showing
- src/main/scala/leon/Evaluator.scala 1 addition, 0 deletionssrc/main/scala/leon/Evaluator.scala
- src/main/scala/leon/FairZ3Solver.scala 29 additions, 1 deletionsrc/main/scala/leon/FairZ3Solver.scala
- src/main/scala/leon/Main.scala 1 addition, 1 deletionsrc/main/scala/leon/Main.scala
- src/main/scala/leon/plugin/CodeExtraction.scala 1 addition, 0 deletionssrc/main/scala/leon/plugin/CodeExtraction.scala
- testcases/regression/invalid/Unit1.scala 7 additions, 0 deletionstestcases/regression/invalid/Unit1.scala
- testcases/regression/valid/Unit1.scala 7 additions, 0 deletionstestcases/regression/valid/Unit1.scala
- testcases/regression/valid/Unit2.scala 7 additions, 0 deletionstestcases/regression/valid/Unit2.scala
Loading
Please register or sign in to comment