mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #3726

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-04 18:48:09 -07:00
parent 10768bd005
commit 7e8753cd3f
2 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_solver.cpp
View file

@ -3910,6 +3910,7 @@ namespace sat {
gc_var(lit.var()); gc_var(lit.var());
} }
m_qhead = 0; m_qhead = 0;
scoped_suspend_rlimit _sp(m_rlimit);
propagate(false); propagate(false);
} }

2
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -621,7 +621,7 @@ private:
} }
} }
catch (tactic_exception & ex) { catch (tactic_exception & ex) {
IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";); IF_VERBOSE(1, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
set_reason_unknown(ex.msg()); set_reason_unknown(ex.msg());
TRACE("sat", tout << "exception: " << ex.msg() << "\n";); TRACE("sat", tout << "exception: " << ex.msg() << "\n";);
m_preprocess = nullptr; m_preprocess = nullptr;