From 91c54f6c392db45e880160cfbad6992bacee1f81 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Jan 2021 14:03:55 -0800 Subject: [PATCH] na --- scripts/mk_win_dist.py | 1 - src/sat/smt/arith_axioms.cpp | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index d540ab48e..3d30d8723 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -89,7 +89,6 @@ def parse_options(): 'x86-only', 'x64-only' ]) - print(options) for opt, arg in options: if opt in ('-b', '--build'): if arg == 'src': diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index f014da9fa..9bdc242b2 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -323,6 +323,7 @@ namespace arith { if (is_eq) { ++m_stats.m_assert_eq; + m_new_eq = true; euf::enode* n1 = var2enode(v1); euf::enode* n2 = var2enode(v2); lpvar w1 = register_theory_var_in_lar_solver(v1); @@ -330,7 +331,6 @@ namespace arith { auto cs = lp().add_equality(w1, w2); add_eq_constraint(cs.first, n1, n2); add_eq_constraint(cs.second, n1, n2); - m_new_eq = true; return; } literal le, ge;