Handle conversion errors gracefully in fair-z3, detect bad ADTs
Showing
- src/main/scala/leon/solvers/ADTManager.scala 62 additions, 32 deletionssrc/main/scala/leon/solvers/ADTManager.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala 11 additions, 6 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 38 additions, 41 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/main/scala/leon/solvers/z3/FairZ3Solver.scala 39 additions, 18 deletionssrc/main/scala/leon/solvers/z3/FairZ3Solver.scala
- src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala 2 additions, 2 deletionssrc/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
Loading
Please register or sign in to comment