mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 12:28:44 +00:00
enable incremental bit-vector solving
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
cc5d719d9e
commit
2bff98ca5d
|
@ -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;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue