mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

#5532

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-04 09:48:46 -07:00
parent 3de9162c7e
commit 051ede64e7
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/sat_dual_solver.cpp
View file

@ -67,6 +67,7 @@ namespace sat {
bool_var w = m_ext2var.get(v, null_bool_var);
if (null_bool_var == w) {
w = m_solver.mk_var();
m_solver.set_external(w);
m_ext2var.setx(v, w, null_bool_var);
m_var2ext.setx(w, v, null_bool_var);
m_vars.push_back(v);
@ -103,6 +104,7 @@ namespace sat {
root = ext2lit(clause[0]);
else {
root = literal(m_solver.mk_var(), false);
m_solver.set_external(root.var());
for (unsigned i = 0; i < sz; ++i)
m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input());
}