Skip to content

Commit d4a4f3b

Browse files
committed
Add URL of Z3 issue for checkAssumptions
1 parent 1b86391 commit d4a4f3b

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,7 @@ trait NonIncrementalSolver extends AbstractSolver { self =>
5252
currentSolver = Some(newSolver)
5353
for (expression <- assertions)
5454
newSolver.assertCnstr(expression)
55+
// we assert the assumptions to address: https://github.com/Z3Prover/z3/issues/5257
5556
for (assumption <- assumptions)
5657
newSolver.assertCnstr(assumption)
5758
val res = newSolver.checkAssumptions(config)(Set())

0 commit comments

Comments
 (0)