mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 03:27:52 +00:00
Code Activity

#5427

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-22 11:33:47 -07:00
parent 9a5c0f2312
commit 76427cd281
3 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/sat/tactic/sat_tactic.cpp
View file

@ -113,8 +113,11 @@ class sat_tactic : public tactic {
break;
}
}
bool euf = m_goal2sat.has_euf();
for (auto* f : fmls_to_validate)
if (md->is_false(f))
if (!euf && md->is_false(f))
IF_VERBOSE(0, verbose_stream() << "failed to validate: " << mk_pp(f, m) << "\n";);
m_goal2sat.update_model(md);