another unsoundness bug

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/polysat/conflict.cpp

@@ -234,6 +234,16 @@ namespace polysat {
         // TODO: check uses of logger().begin_conflict(). sometimes we call it before adding constraints, sometimes after...
     }
 
+    void conflict::init(dependency dep, signed_constraint c) {
+        SASSERT(empty());
+        m_level = s.m_level;
+        m_dep = dep;
+        SASSERT(!empty());
+        insert_vars(c);
+        logger().begin_conflict();
+    }
+
+
     void conflict::init(signed_constraint c) {
         LOG("Conflict: constraint " << lit_pp(s, c));
         SASSERT(empty());

src/math/polysat/conflict.h

@@ -139,6 +139,11 @@ namespace polysat {
         /** conflict because there is no viable value for the variable v, by fallback solver */
         void init_by_viable_fallback(pvar v, univariate_solver& us);
 
+        /** conflict depends on dep and free variables in c **/
+        /** c evaluates to false but is assigned to true by dep **/
+        void init(dependency dep, signed_constraint c);
+
+
         bool contains(signed_constraint c) const { SASSERT(c); return contains(c.blit()); }
         bool contains(sat::literal lit) const;
         bool contains_pvar(pvar v) const { return m_vars.contains(v); }

src/math/polysat/solver.cpp

@@ -184,8 +184,10 @@ namespace polysat {
         m_bvars.assumption(lit, m_level, dep);
         m_trail.push_back(trail_instr_t::assign_bool_i);
         m_search.push_boolean(lit);
-        if (c.is_currently_false(*this))
+
-            set_conflict(c);
+        if (c.is_currently_false(*this)) 
+            // conflict depends on dep, and free variables in c
+            set_conflict(dep, c);
     }
 
     bool solver::can_propagate() {

src/math/polysat/solver.h

@@ -282,6 +282,7 @@ namespace polysat {
         bool repropagate(sat::literal lit, clause& cl);
         void propagate_clause(clause& cl);
 
+        void set_conflict(dependency dep, signed_constraint c) { m_conflict.init(dep, c); }
         void set_conflict_at_base_level(dependency dep) { m_conflict.init_at_base_level(dep); }
         void set_conflict(signed_constraint c) { m_conflict.init(c); }
         void set_conflict(clause& cl) { m_conflict.init(cl); }