Termination checker fixes for new DefOps and theory encoders
Showing
- src/main/scala/leon/purescala/DefOps.scala 5 additions, 3 deletionssrc/main/scala/leon/purescala/DefOps.scala
- src/main/scala/leon/solvers/cvc4/CVC4UnrollingSolver.scala 1 addition, 1 deletionsrc/main/scala/leon/solvers/cvc4/CVC4UnrollingSolver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala 4 additions, 1 deletionsrc/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala 1 addition, 1 deletionsrc/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala 2 additions, 1 deletionsrc/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
- src/main/scala/leon/solvers/theories/BagEncoder.scala 1 addition, 1 deletionsrc/main/scala/leon/solvers/theories/BagEncoder.scala
- src/main/scala/leon/solvers/theories/StringEncoder.scala 1 addition, 1 deletionsrc/main/scala/leon/solvers/theories/StringEncoder.scala
- src/main/scala/leon/solvers/theories/TheoryEncoder.scala 1 addition, 1 deletionsrc/main/scala/leon/solvers/theories/TheoryEncoder.scala
- src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala 5 additions, 4 deletionssrc/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
- src/main/scala/leon/solvers/z3/FairZ3Solver.scala 1 addition, 1 deletionsrc/main/scala/leon/solvers/z3/FairZ3Solver.scala
- src/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala 1 addition, 1 deletionsrc/main/scala/leon/solvers/z3/Z3UnrollingSolver.scala
- src/main/scala/leon/termination/ChainProcessor.scala 3 additions, 3 deletionssrc/main/scala/leon/termination/ChainProcessor.scala
- src/main/scala/leon/termination/Processor.scala 8 additions, 14 deletionssrc/main/scala/leon/termination/Processor.scala
Loading
Please register or sign in to comment