mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

close #4450

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-04 09:22:38 -07:00
parent 57086edc42
commit e52eed325c
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -963,6 +963,8 @@ private:
for (expr * f : m_fmls) {
expr_ref tmp(m);
eval(f, tmp);
if (m.limit().is_canceled())
return;
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n";
model_smt2_pp(tout, m, *(mdl.get()), 0););