#6654

fix reflexivity for tree-order
Z3Prover · Mar 31, 2023 · e0a066e · e0a066e
1 parent 7664429
commit e0a066e
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp
@@ -405,6 +405,12 @@ namespace smt {
                 TRACE("special_relations", tout << "already: " << a.v2() << " <= " << a.v1() << "\n";);
                 continue;
             }
+            if (a.v1() == a.v2()) {
+                r.m_explanation.reset();
+                r.m_explanation.push_back(a.explanation());
+                set_conflict(r);                
+                return l_false;
+            }
             // the nodes visited from v1 become target for v2
             if (r.m_graph.reachable(a.v2(), visited, target, w)) {
                 //