diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index d79aeffde..32cc877dd 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -678,7 +678,7 @@ namespace sat { for (literal u : succ) { SASSERT(u != l); // l => u - if (u.index() > l.index() && is_stamped(u)) { + if (u.index() > (~l).index() && is_stamped(u)) { add_arc(~l, ~u); add_arc( u, l); } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 7c703653c..75231f274 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -921,7 +921,7 @@ struct sat2goal::imp { } } } - + virtual void operator()(model_ref & md) { TRACE("sat_mc", tout << "before sat_mc\n"; model_v2_pp(tout, *md); display(tout);); // REMARK: potential problem