mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-28 07:42:27 -07:00
parent 2475f3bff5
commit 7764148dd3
1 changed files with 0 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_context.cpp
View file

@ -3778,14 +3778,8 @@ namespace smt {
#ifdef Z3DEBUG #ifdef Z3DEBUG
for (unsigned i = 0; i < num_lits; i++) { for (unsigned i = 0; i < num_lits; i++) {
literal l = lits[i]; literal l = lits[i];
<<<<<<< HEAD
expr* real_atom;
if (expr_signs[i] != l.sign()) {
=======
if (expr_signs[i] != l.sign()) { if (expr_signs[i] != l.sign()) {
expr* real_atom; expr* real_atom;
>>>>>>> f1412d3f3249529224f4180f601652da210b274a
VERIFY(m_manager.is_not(expr_lits.get(i), real_atom)); VERIFY(m_manager.is_not(expr_lits.get(i), real_atom));
// the sign must have flipped when internalizing // the sign must have flipped when internalizing
CTRACE("resolve_conflict_bug", real_atom != bool_var2expr(l.var()), tout << mk_pp(real_atom, m_manager) << "\n" << mk_pp(bool_var2expr(l.var()), m_manager) << "\n";); CTRACE("resolve_conflict_bug", real_atom != bool_var2expr(l.var()), tout << mk_pp(real_atom, m_manager) << "\n" << mk_pp(bool_var2expr(l.var()), m_manager) << "\n";);