Merge pull request #149 from jad-hamza/incremental

Avoid using checkAssumptions in non-incremental mode

Author: samarion

src/main/scala/inox/solvers/combinators/NonIncrementalSolver.scala

@@ -52,7 +52,10 @@ trait NonIncrementalSolver extends AbstractSolver { self =>
       currentSolver = Some(newSolver)
       for (expression <- assertions)
         newSolver.assertCnstr(expression)
-      val res = newSolver.checkAssumptions(config)(assumptions)
+      // we assert the assumptions to address: https://github.com/Z3Prover/z3/issues/5257
+      for (assumption <- assumptions)
+        newSolver.assertCnstr(assumption)
+      val res = newSolver.checkAssumptions(config)(Set())
       currentSolver = None
       res
     } finally {