From 2bff98ca5d5930eef48e2e0c99a0a93e8ad725be Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 1 Sep 2015 09:52:48 -0700 Subject: [PATCH] enable incremental bit-vector solving Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 4c0318c22..0ecda2808 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -881,7 +881,7 @@ namespace sat { bool solver::check_inconsistent() { if (inconsistent()) { - if (tracking_assumptions() || !m_user_scope_literals.empty()) + if (tracking_assumptions()) resolve_conflict(); return true; }