mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

fix update to variables

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-28 14:39:16 -08:00
parent 0b424942ab
commit b1724b2f62
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -926,7 +926,7 @@ model_converter* sat2goal::mc::translate(ast_translation& translator) {
void sat2goal::mc::collect(ast_pp_util& visitor) {
flush_gmc();
collect(visitor);
if (m_gmc) m_gmc->collect(visitor);
}
void sat2goal::mc::display(std::ostream& out) {
@ -995,6 +995,10 @@ void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) {
}
expr_ref sat2goal::mc::lit2expr(sat::literal l) {
if (!m_var2expr.get(l.var())) {
app* aux = m.mk_fresh_const(0, m.mk_bool_sort());
m_var2expr.set(l.var(), aux);
}
VERIFY(m_var2expr.get(l.var()));
expr_ref result(m_var2expr.get(l.var()), m);
if (l.sign()) {