fix #6091

src/sat/sat_drat.cpp

@@ -217,7 +217,7 @@ namespace sat {
             return;
         
         if (m_check_unsat) {
-            assign_propagate(l);
+            assign_propagate(l, nullptr);
             m_units.push_back({l, nullptr});
         }
     }
@@ -249,9 +249,9 @@ namespace sat {
             if (value(l1) == l_false && value(l2) == l_false) 
                 m_inconsistent = true;            
             else if (value(l1) == l_false) 
-                assign_propagate(l2);            
+                assign_propagate(l2, &c);            
             else if (value(l2) == l_false) 
-                assign_propagate(l1);            
+                assign_propagate(l1, &c);            
         }
     }
 
@@ -319,7 +319,7 @@ namespace sat {
             m_inconsistent = true;
             break;
         case 1:            
-            assign_propagate(l1);
+            assign_propagate(l1, &c);
             break;
         default: {
             SASSERT(num_watch == 2);
@@ -363,7 +363,7 @@ namespace sat {
         unsigned num_units = m_units.size();
         for (unsigned i = 0; !m_inconsistent && i < n; ++i) {
             declare(c[i]);
-            assign_propagate(~c[i]);
+            assign_propagate(~c[i], nullptr);
         }
 
         for (unsigned i = num_units; i < m_units.size(); ++i) 
@@ -384,7 +384,7 @@ namespace sat {
             return false;
         unsigned num_units = m_units.size();
         for (unsigned i = 0; !m_inconsistent && i < n; ++i) 
-            assign_propagate(~c[i]);
+            assign_propagate(~c[i], nullptr);
         
         DEBUG_CODE(if (!m_inconsistent) validate_propagation(););        
         DEBUG_CODE(
@@ -595,7 +595,7 @@ namespace sat {
         return val == l_undef || !l.sign() ? val : ~val;
     }
 
-    void drat::assign(literal l) {
+    void drat::assign(literal l, clause* c) {
         lbool new_value = l.sign() ? l_false : l_true;
         lbool old_value = value(l);
         //        TRACE("sat_drat", tout << "assign " << l << " := " << new_value << " from " << old_value << "\n";);
@@ -607,16 +607,16 @@ namespace sat {
             break;
         case l_undef:
             m_assignment.setx(l.var(), new_value, l_undef);
-            m_units.push_back({l, nullptr});
+            m_units.push_back({l, c});
             break;
         }
     }
 
-    void drat::assign_propagate(literal l) {
+    void drat::assign_propagate(literal l, clause* c) {
         if (!m_check_unsat)
             return;
         unsigned num_units = m_units.size();
-        assign(l);
+        assign(l, c);
         for (unsigned i = num_units; !m_inconsistent && i < m_units.size(); ++i) 
             propagate(m_units[i].first);        
     }
@@ -661,7 +661,7 @@ namespace sat {
                 else {
                     *it2 = *it;
                     it2++;
-                    assign(wc.m_l1);
+                    assign(wc.m_l1, &c);
                 }
             }
         }

src/sat/sat_drat.h

@@ -105,9 +105,9 @@ namespace sat {
         status get_status(bool learned) const;
 
         void declare(literal l);
-        void assign(literal l);
+        void assign(literal l, clause* c);
         void propagate(literal l);
-        void assign_propagate(literal l);
+        void assign_propagate(literal l, clause* c);
         void del_watch(clause& c, literal l);
         bool is_drup(unsigned n, literal const* c);
         bool is_drat(unsigned n, literal const* c);

src/smt/theory_arith.h

@@ -974,7 +974,7 @@ namespace smt {
         /**
            \brief A monomial is 'pure' if does not have a numeric coefficient.
         */
-        bool is_pure_monomial(expr * m) const { return m_util.is_mul(m) && (to_app(m)->get_num_args() > 2 || !m_util.is_numeral(to_app(m)->get_arg(0))); }
+        bool is_pure_monomial(expr * m) const;
         bool is_pure_monomial(theory_var v) const { return is_pure_monomial(get_enode(v)->get_expr()); }
         void mark_var(theory_var v, svector<theory_var> & vars, var_set & already_found);
         void mark_dependents(theory_var v, svector<theory_var> & vars, var_set & already_found, row_set & already_visited_rows);

src/smt/theory_arith_nl.h

@@ -624,11 +624,9 @@ template<typename Ext>
 bool theory_arith<Ext>::check_monomial_assignments() {
     bool computed_epsilon = false;
     for (theory_var v : m_nl_monomials) {
-        TRACE("non_linear", tout << "v" << v << " is relevant: " << ctx.is_relevant(get_enode(v)) << "\n";
+        TRACE("non_linear", tout << "v" << v << " is relevant: " << ctx.is_relevant(get_enode(v)) << "\n");
-              tout << "check_monomial_assignments result: " << check_monomial_assignment(v, computed_epsilon) << "\n";
-              tout << "computed_epsilon: " << computed_epsilon << "\n";);
         if (ctx.is_relevant(get_enode(v)) && !check_monomial_assignment(v, computed_epsilon)) {
-            TRACE("non_linear_failed", tout << "check_monomial_assignment failed for:\n" << mk_ismt2_pp(var2expr(v), get_manager()) << "\n";
+            TRACE("non_linear", tout << "check_monomial_assignment failed for:\n" << mk_ismt2_pp(var2expr(v), get_manager()) << "\n";
                   display_var(tout, v););                
             return false;
         }
@@ -1254,6 +1252,17 @@ bool theory_arith<Ext>::in_monovariate_monomials(buffer<coeff_expr> & p, expr *
 }
 
 
+template<typename Ext>
+bool theory_arith<Ext>::is_pure_monomial(expr* mon) const {
+    if (!m_util.is_mul(mon))
+        return false;
+    app* p = to_app(mon);
+    for (expr* arg : *p)
+        if (m_util.is_numeral(arg) || m_util.is_mul(arg))
+            return false;
+    return true;
+}
+
 /**
    \brief Display a nested form expression
 */