change signed projection to include root object.

Z3Prover · Mar 23, 2024 · c18a42c · c18a42c
1 parent 80642e5
commit c18a42c
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 3 deletions.
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
@@ -1744,7 +1744,16 @@ namespace nlsat {
                     solve_eq(x, eq_index, ps);
                 }
                 else {
-                    project_pairs(x, eq_index, ps);
+                    add_zero_assumption(p);
+
+                    for (unsigned j = 0; j < ps.size(); ++j) {
+                        if (j == eq_index)
+                            continue;
+                        p = ps.get(j);
+                        int s = sign(p);
+                        atom::kind k = (s == 0)?(atom::EQ):((s < 0)?(atom::LT):(atom::GT));
+                        add_simple_assumption(k, p, false);
+                    }
                 }
                 return;
             }

diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
@@ -480,8 +480,10 @@ namespace qe {
                 num_scopes = 2*(level()/2);
             }
             else {
-                SASSERT(clevel.max() + 2 <= level());
-                num_scopes = level() - clevel.max();
+                if (clevel.max() + 2 <= level())                    
+                    num_scopes = level() - clevel.max();
+                else
+                    num_scopes = 2; // the projection contains auxiliary variables from root objects.
                 SASSERT(num_scopes >= 2);
             }