fix #3004

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Feb 18, 2020 · f810f25 · f810f25
1 parent 1959b7c
commit f810f25
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 11 deletions.
diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp
@@ -157,10 +157,8 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
 
     if (is_forall(e)) {
         quantifier * q = to_quantifier(e);
-        expr * qe = q->get_expr();
-        if ((m_manager.is_eq(qe))) {
-            expr * lhs = to_app(qe)->get_arg(0);
-            expr * rhs = to_app(qe)->get_arg(1);
+        expr * qe = q->get_expr(), *lhs = nullptr, *rhs = nullptr;
+        if ((m_manager.is_eq(qe, lhs, rhs))) {
 
             if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) &&
                 !depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) {
@@ -173,9 +171,9 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
                 t = lhs;
                 return true;
             }
-        } else if (m_manager.is_not(qe) && is_non_ground_uninterp(to_app(qe)->get_arg(0)) &&
-                   is_unique(to_app(to_app(qe)->get_arg(0))->get_decl())) { // this is like f(...) = false
-            a = to_app(to_app(qe)->get_arg(0));
+        } else if (m_manager.is_not(qe, lhs) && is_non_ground_uninterp(lhs) &&
+                   is_unique(to_app(lhs)->get_decl())) { // this is like f(...) = false
+            a = to_app(lhs);
             t = m_manager.mk_false();
             return true;
         } else if (is_non_ground_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true

diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
@@ -690,7 +690,7 @@ namespace datalog {
     void context::reopen() {
         SASSERT(m_closed);
         m_rule_set.reopen();
-        m_closed = false;
+        m_closed = false;        
     }
 
     void context::transform_rules(rule_transformer::plugin* plugin) {

diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
@@ -74,7 +74,7 @@ namespace datalog {
         }
 
         ~scoped_query() {
-            m_ctx.reopen();                                
+            m_ctx.ensure_opened();                                
             m_ctx.restrict_predicates(m_preds);
             m_ctx.replace_rules(m_rules);
             if (m_was_closed) {

diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp
@@ -58,7 +58,7 @@ class quasi_macros_tactic : public tactic {
                 deps.push_back(g->dep(i));
             }
 
-            while (more) { // CMW: use repeat(...) ?
+            do { 
                 if (m().canceled())
                     throw tactic_exception(m().limit().get_cancel_msg());
 
@@ -69,7 +69,8 @@ class quasi_macros_tactic : public tactic {
                 forms.swap(new_forms);
                 proofs.swap(new_proofs);
                 deps.swap(new_deps);
-            }
+            } 
+            while (more);
 
             g->reset();
             for (unsigned i = 0; i < new_forms.size(); i++)