From 20fe08d80cdfcfa3c47c584a3f1c7269b30b7068 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 4 Feb 2018 09:51:45 -0800
Subject: [PATCH] fix more bugs with compilation of pb equalities

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/ba_solver.cpp                |  2 +-
 src/sat/tactic/goal2sat.cpp          | 17 +++++++++--------
 src/tactic/arith/lia2card_tactic.cpp | 17 +----------------
 3 files changed, 11 insertions(+), 25 deletions(-)

diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 653e578a3..ac332d362 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -1571,7 +1571,7 @@ namespace sat {
             m_constraints.push_back(c);
         }
         literal lit = c->lit();
-        if (c->learned() && !s().at_base_lvl()) {
+        if (c->learned() && m_solver && !s().at_base_lvl()) {
             SASSERT(lit == null_literal);
             // gets initialized after backjump.
             m_constraint_to_reinit.push_back(c);
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index b84a64651..5bba70659 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -495,8 +495,8 @@ struct goal2sat::imp {
         SASSERT(k.is_unsigned());
         svector<wliteral> wlits;
         convert_pb_args(t, wlits);
-        sat::bool_var v1 = root ? sat::null_bool_var : m_solver.mk_var(true);
-        sat::bool_var v2 = root ? sat::null_bool_var : m_solver.mk_var(true);
+        sat::bool_var v1 = (root && !sign) ? sat::null_bool_var : m_solver.mk_var(true);
+        sat::bool_var v2 = (root && !sign) ? sat::null_bool_var : m_solver.mk_var(true);
         m_ext->add_pb_ge(v1, wlits, k.get_unsigned());        
         k.neg();
         for (wliteral& wl : wlits) {
@@ -505,7 +505,7 @@ struct goal2sat::imp {
         }
         check_unsigned(k);
         m_ext->add_pb_ge(v2, wlits, k.get_unsigned());
-        if (root) {
+        if (root && !sign) {
             m_result_stack.reset();
         }
         else {
@@ -516,7 +516,8 @@ struct goal2sat::imp {
             mk_clause(~l, l2);
             mk_clause(~l1, ~l2, l);
             m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
-            m_result_stack.push_back(l);
+            m_result_stack.push_back(sign ? ~l : l);
+            if (root) mk_clause(~l);
         }
     }
 
@@ -564,8 +565,8 @@ struct goal2sat::imp {
         SASSERT(k.is_unsigned());
         sat::literal_vector lits;
         convert_pb_args(t->get_num_args(), lits);
-        sat::bool_var v1 = root ? sat::null_bool_var : m_solver.mk_var(true);
-        sat::bool_var v2 = root ? sat::null_bool_var : m_solver.mk_var(true);
+        sat::bool_var v1 = (root && !sign) ? sat::null_bool_var : m_solver.mk_var(true);
+        sat::bool_var v2 = (root && !sign) ? sat::null_bool_var : m_solver.mk_var(true);
         m_ext->add_at_least(v1, lits, k.get_unsigned());        
         for (sat::literal& l : lits) {
             l.neg();
@@ -573,7 +574,7 @@ struct goal2sat::imp {
         m_ext->add_at_least(v2, lits, lits.size() - k.get_unsigned());
 
 
-        if (root) {
+        if (root && !sign) {
             m_result_stack.reset();
         }
         else {
@@ -585,7 +586,7 @@ struct goal2sat::imp {
             mk_clause(~l1, ~l2, l);
             m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
             m_result_stack.push_back(sign ? ~l : l);
-
+            if (root) mk_clause(~l);
         }
     }
 
diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index dd9c5ff6b..18acde8a8 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -103,21 +103,6 @@ class lia2card_tactic : public tactic {
             }
             TRACE("pbsum", tout << expr_ref(m.mk_app(f, sz, es), m) << " ==>\n" <<  result << "\n";);
 
-#if 0
-            expr_ref vc(m);
-            vc = m.mk_not(m.mk_eq(m.mk_app(f, sz, es), result));
-            ast_pp_util pp(m);
-            pp.collect(vc);
-            std::cout 
-                << "(push)\n"
-                << "(echo \"" << result << "\")\n"
-                ;
-            pp.display_decls(std::cout);
-            std::cout
-                << "(assert " << vc << ")\n"
-                << "(check-sat)\n"
-                << "(pop)\n";
-#endif
             return BR_DONE;
         }
 
@@ -237,7 +222,7 @@ public:
         result.push_back(g.get());
         TRACE("pb", g->display(tout););
         SASSERT(g->is_well_sorted());
-        m_bounds.reset();        
+        m_bounds.reset();   
     }
     
     expr* mk_le(unsigned sz, rational const* weights, expr* const* args, rational const& w) {