mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

force push

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-03 11:38:33 -08:00
parent 69070a7486
commit 79ababb00a
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/sat/tactic/goal2sat.cpp
View file

@ -280,7 +280,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
void cache(app* t, sat::literal l) override {
SASSERT(m_num_scopes == 0);
force_push();
SASSERT(!m_app2lit.contains(t));
SASSERT(!m_lit2app.contains(l.index()));
m_app2lit.insert(t, l);
@ -817,6 +817,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
sat::literal result = m_result_stack.back();
m_result_stack.pop_back();
if (!result.sign() && m_map.to_bool_var(n) == sat::null_bool_var) {
force_push();
m_map.insert(n, result.var());
m_solver.set_external(result.var());
}