fix case for 0 multiplier in monomial_bounds

disabled in master - it violates invariants in the lra solver.

src/math/lp/monomial_bounds.cpp

@@ -276,7 +276,7 @@ namespace nla {
         
         rational k = fixed_var_product(m);
         lpvar w = non_fixed_var(m);
-        if (w == null_lpvar)
+        if (w == null_lpvar || k == 0)
             propagate_fixed(m, k);
         else
             propagate_nonfixed(m, k, w);
@@ -293,6 +293,10 @@ namespace nla {
 
     void monomial_bounds::propagate_fixed(monic const& m, rational const& k) {
         auto* dep = explain_fixed(m, k);
+        if (!c().lra.is_base(m.var())) {
+            lp::impq val(k);
+            c().lra.set_value_for_nbasic_column(m.var(), val);
+        }
         c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep);
         // propagate fixed equality
         auto exp = get_explanation(dep);
@@ -300,6 +304,7 @@ namespace nla {
     }
 
     void monomial_bounds::propagate_nonfixed(monic const& m, rational const& k, lpvar w) {
+        VERIFY(k != 0);
         vector<std::pair<lp::mpq, unsigned>> coeffs;        
         coeffs.push_back(std::make_pair(-k, w));
         coeffs.push_back(std::make_pair(rational::one(), m.var()));

src/sat/smt/euf_proof_checker.cpp

@@ -501,8 +501,9 @@ namespace euf {
         for (expr* arg : clause)
             std::cout << "\n " << mk_bounded_pp(arg, m);
         std::cout << ")\n";
+        std::cout.flush();
 
-        if (is_rup(proof_hint)) 
+        if (false && is_rup(proof_hint)) 
             diagnose_rup_failure(clause);
             
         add_clause(clause);
@@ -527,9 +528,6 @@ namespace euf {
             for (expr* f : core)
                 std::cout << mk_pp(f, m) << "\n";
         }
-        SASSERT(false);
-        
-        exit(0);
     }
 
     void smt_proof_checker::collect_statistics(statistics& st) const {

src/smt/smt_clause_proof.cpp

@@ -90,14 +90,14 @@ namespace smt {
         return proof_ref(m);
     }
 
-    void clause_proof::add(clause& c) {
+    void clause_proof::add(clause& c, literal_buffer const* simp_lits) {
         if (!is_enabled())
             return;
         justification* j = c.get_justification();
         auto st = kind2st(c.get_kind());
         auto pr = justification2proof(st, j);
         CTRACE("mk_clause", pr.get(), tout << mk_bounded_pp(pr, m, 4) << "\n";);
-        update(c, st, pr);        
+        update(c, st, pr, simp_lits);        
     }
 
     void clause_proof::add(unsigned n, literal const* lits, clause_kind k, justification* j) {
@@ -137,12 +137,15 @@ namespace smt {
         update(st, m_lits, pr);
     }
 
-    void clause_proof::add(literal lit1, literal lit2, clause_kind k, justification* j) {
+    void clause_proof::add(literal lit1, literal lit2, clause_kind k, justification* j, literal_buffer const* simp_lits) {
         if (!is_enabled())
             return;
         m_lits.reset();
         m_lits.push_back(ctx.literal2expr(lit1));
         m_lits.push_back(ctx.literal2expr(lit2));
+        if (simp_lits) 
+            for (auto lit : *simp_lits)
+                m_lits.push_back(ctx.literal2expr(~lit));
         auto st = kind2st(k);
         auto pr = justification2proof(st, j);
         update(st, m_lits, pr);
@@ -160,7 +163,7 @@ namespace smt {
     }
 
     void clause_proof::del(clause& c) {
-        update(c, status::deleted, justification2proof(status::deleted, nullptr));
+        update(c, status::deleted, justification2proof(status::deleted, nullptr), nullptr);
     }
 
     std::ostream& clause_proof::display_literals(std::ostream& out, expr_ref_vector const& v) {
@@ -191,6 +194,8 @@ namespace smt {
             m_trail.push_back(info(st, v, p));
         if (m_on_clause_eh) 
             m_on_clause_eh(m_on_clause_ctx, p, 0, nullptr, v.size(), v.data());
+        static unsigned s_count = 0;
+        
         if (m_has_log) {
             init_pp_out();
             auto& out = *m_pp_out;
@@ -220,12 +225,15 @@ namespace smt {
         }
     }
 
-    void clause_proof::update(clause& c, status st, proof* p) {
+    void clause_proof::update(clause& c, status st, proof* p, literal_buffer const* simp_lits) {
         if (!is_enabled())
             return;
         m_lits.reset();
         for (literal lit : c) 
             m_lits.push_back(ctx.literal2expr(lit));
+        if (simp_lits) 
+            for (auto lit : *simp_lits)
+                m_lits.push_back(ctx.literal2expr(~lit));
         update(st, m_lits, p);        
     }
 

src/smt/smt_clause_proof.h

@@ -68,7 +68,7 @@ namespace smt {
         void init_pp_out();
         
         void update(status st, expr_ref_vector& v, proof* p);
-        void update(clause& c, status st, proof* p);
+        void update(clause& c, status st, proof* p, literal_buffer const* simp_lits);
         status kind2st(clause_kind k);
         proof_ref justification2proof(status st, justification* j);
         void log(status st, proof* p);
@@ -79,8 +79,8 @@ namespace smt {
         clause_proof(context& ctx);
         void shrink(clause& c, unsigned new_size);
         void add(literal lit, clause_kind k, justification* j);
-        void add(literal lit1, literal lit2, clause_kind k, justification* j);
+        void add(literal lit1, literal lit2, clause_kind k, justification* j, literal_buffer const* simp_lits = nullptr);
-        void add(clause& c);
+        void add(clause& c, literal_buffer const* simp_lits = nullptr);
         void add(unsigned n, literal const* lits, clause_kind k, justification* j);
         void propagate(literal lit, justification const& j, literal_vector const& ante);
         void del(clause& c);

src/smt/smt_internalizer.cpp

@@ -1378,12 +1378,12 @@ namespace smt {
     clause * context::mk_clause(unsigned num_lits, literal * lits, justification * j, clause_kind k, clause_del_eh * del_eh) {
         TRACE("mk_clause", display_literals_verbose(tout << "creating clause: " << literal_vector(num_lits, lits) << "\n", num_lits, lits) << "\n";);
         m_clause_proof.add(num_lits, lits, k, j);
+        literal_buffer simp_lits;
         switch (k) {
         case CLS_TH_AXIOM:
             dump_axiom(num_lits, lits);
             Z3_fallthrough;
         case CLS_AUX: {
-            literal_buffer simp_lits;
             if (m_searching)
                 dump_lemma(num_lits, lits);
             if (!simplify_aux_clause_literals(num_lits, lits, simp_lits)) {
@@ -1451,7 +1451,7 @@ namespace smt {
                 else if (get_assignment(l2) == l_false) {
                     assign(l1, b_justification(~l2));
                 }
-                m_clause_proof.add(l1, l2, k, j);
+                m_clause_proof.add(l1, l2, k, j, &simp_lits);
                 m_stats.m_num_mk_bin_clause++;
                 return nullptr;
             }
@@ -1464,7 +1464,7 @@ namespace smt {
             bool reinit         = save_atoms;
             SASSERT(!lemma || j == 0 || !j->in_region());
             clause * cls = clause::mk(m, num_lits, lits, k, j, del_eh, save_atoms, m_bool_var2expr.data());
-            m_clause_proof.add(*cls);
+            m_clause_proof.add(*cls, &simp_lits);
             if (lemma) {
                 cls->set_activity(activity);
                 if (k == CLS_LEARNED) {

src/smt/theory_lra.cpp

@@ -2112,7 +2112,8 @@ public:
     bool propagate_core() {
         m_model_is_initialized = false;
         flush_bound_axioms();
-        // disabled in master: propagate_nla(); 
+        // disabled in master:
+        // propagate_nla(); 
         if (!can_propagate_core())
             return false;
         m_new_def = false;        
@@ -2161,6 +2162,8 @@ public:
     }
 
     void add_equalities() {
+        if (!propagate_eqs()) 
+            return;
         for (auto const& [v,k,e] : m_nla->fixed_equalities())
             add_equality(v, k, e);
         for (auto const& [i,j,e] : m_nla->equalities())
@@ -2168,7 +2171,7 @@ public:
     }
 
     void add_equality(lpvar j, rational const& k, lp::explanation const& exp) {
-        verbose_stream() << "equality " << j << " " << k << "\n";
+        //verbose_stream() << "equality " << j << " " << k << "\n";
         TRACE("arith", tout << "equality " << j << " " << k << "\n");
         theory_var v;
         if (k == 1)
@@ -3174,8 +3177,7 @@ public:
         std::function<expr*(void)> fn = [&]() { return m.mk_eq(x->get_expr(), y->get_expr()); };
         scoped_trace_stream _sts(th, fn);
 
-       
+        //VERIFY(validate_eq(x, y));
-        // SASSERT(validate_eq(x, y));
         ctx().assign_eq(x, y, eq_justification(js));
     }
     
@@ -3289,6 +3291,7 @@ public:
         for (auto ev : m_explanation) 
             set_evidence(ev.ci(), m_core, m_eqs);
 
+        
         // SASSERT(validate_conflict(m_core, m_eqs));
         if (is_conflict) {
             ctx().set_conflict(
@@ -3543,6 +3546,8 @@ public:
         lbool r = nctx.check();
         if (r == l_true) {
             nctx.display_asserted_formulas(std::cout);
+            std::cout.flush();
+            std::cout.flush();
         }
         return l_true != r;
     }