From e45ae326857aefeb711c2655f20ba93519bfc5c2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 8 Dec 2021 09:02:05 -0800
Subject: [PATCH] unsound equality propagation #5676

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_axioms.cpp   |  2 +-
 src/math/lp/lp_bound_propagator.h | 31 ++++++++++++++++++++++---------
 2 files changed, 23 insertions(+), 10 deletions(-)

diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index 2e2a0cff2..55d58e3f7 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -1034,7 +1034,7 @@ namespace seq {
      * Assume that r has the property that if r accepts string p
      * then r does *not* accept any suffix of p. It is conceptually easy to 
      * convert a deterministic automaton for a regex to a suffix blocking acceptor
-     * by redirecting removing outgoing edges from accepting states and redirecting them
+     * by removing outgoing edges from accepting states and redirecting them
      * to a sink. Alternative, introduce a different string membership predicate that is 
      * prefix sensitive. 
      *
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index dfe7227e6..45d9f0296 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -116,30 +116,43 @@ class lp_bound_propagator {
 
 
     map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>>  m_val2fixed_row;
+
+    bool is_fixed_row(unsigned r, unsigned & x) {
+        x = UINT_MAX;
+        const auto & row = lp().get_row(r);
+        for (unsigned k = 0; k < row.size(); k++) {
+            const auto& c = row[k];
+            if (column_is_fixed(c.var()))
+                continue;
+            if (x != UINT_MAX)
+                return false;
+            x = c.var();
+        }
+        return x != UINT_MAX;
+    }
     
-    void try_add_equation_with_internal_fixed_tables(unsigned r1, vertex const* v) {
+    void try_add_equation_with_internal_fixed_tables(unsigned r1) {
         SASSERT(m_fixed_vertex);
-        if (v != m_root)
+        unsigned v1, v2;
+        if (!is_fixed_row(r1, v1))
             return;
-        unsigned v1 = v->column();
         unsigned r2 = UINT_MAX;
         if (!m_val2fixed_row.find(val(v1), r2) || r2 >= lp().row_count()) {
             m_val2fixed_row.insert(val(v1), r1);
             return;
         }
-        unsigned v2, v3;
-        int polarity;
-        if (!is_tree_offset_row(r2, v2, v3, polarity) || !not_set(v3) ||
-            is_int(v1) != is_int(v2) || val(v1) != val(v2)) {
+        if (!is_fixed_row(r2, v2) || val(v1) != val(v2) || is_int(v1) != is_int(v2)) {
             m_val2fixed_row.insert(val(v1), r1);
             return;
         }
         if (v1 == v2)
             return;
-        
+
+        TRACE("eq", tout << v1 << " = " << v2 << "\n");
         explanation ex;
         explain_fixed_in_row(r1, ex);
         explain_fixed_in_row(r2, ex);
+        TRACE("eq", print_row(tout, r1); print_row(tout, r2); tout << v1 << " == " << v2 << " = " << val(v1) << "\n");
         add_eq_on_columns(ex, v1, v2, true);
     }
     
@@ -148,7 +161,7 @@ class lp_bound_propagator {
         unsigned v_j = v->column();
         unsigned j = null_lpvar;
         if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) {
-            try_add_equation_with_internal_fixed_tables(row_index, v);
+            try_add_equation_with_internal_fixed_tables(row_index);
             return;
         }