#5336

src/ast/rewriter/var_subst.cpp

@@ -17,6 +17,7 @@ Notes:
 
 --*/
 #include "ast/rewriter/var_subst.h"
+#include "ast/rewriter/expr_safe_replace.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_smt2_pp.h"
@@ -24,7 +25,8 @@ Notes:
 #include "ast/for_each_expr.h"
 
 expr_ref var_subst::operator()(expr * n, unsigned num_args, expr * const * args) {
-    expr_ref result(m_reducer.m());
+    ast_manager& m = m_reducer.m();
+    expr_ref result(m);
     if (is_ground(n) || num_args == 0) {
         result = n;
         //application does not have free variables or nested quantifiers.
@@ -40,6 +42,13 @@ expr_ref var_subst::operator()(expr * n, unsigned num_args, expr * const * args)
 
         return result;
     }
+    if (has_quantifiers(n)) {
+        expr_safe_replace rep(m);
+        for (unsigned k = 0; k < num_args; ++k)
+            rep.insert(m.mk_var(m_std_order ? num_args - k - 1 : k, args[k]->get_sort()), args[k]);
+        rep(n, result);
+        return result;
+    }
     SASSERT(is_well_sorted(result.m(), n));
     m_reducer.reset();
     if (m_std_order)
@@ -47,10 +56,10 @@ expr_ref var_subst::operator()(expr * n, unsigned num_args, expr * const * args)
     else
         m_reducer.set_bindings(num_args, args);
     m_reducer(n, result);
-    SASSERT(is_well_sorted(m_reducer.m(), result));
+    SASSERT(is_well_sorted(m, result));
     TRACE("var_subst_bug",
-          tout << "m_std_order: " << m_std_order << "\n" << mk_ismt2_pp(n, m_reducer.m()) << "\nusing\n";
-          for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m_reducer.m()) << "\n";
+          tout << "m_std_order: " << m_std_order << "\n" << mk_ismt2_pp(n, m) << "\nusing\n";
+          for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m) << "\n";
           tout << "\n------>\n";
           tout << result << "\n";);
     return result;

src/sat/smt/q_mbi.cpp

@@ -146,7 +146,7 @@ namespace q {
             return l_undef;
         if (m.is_false(qb->mbody))
             return l_true;
-        if (quick_check(q, *qb))
+        if (quick_check(q, q_flat, *qb))
             return l_false;
 
         m_generation_bound = 0;
@@ -471,18 +471,20 @@ namespace q {
         }
     }
 
-    bool mbqi::quick_check(quantifier* q, q_body& qb) {
+    bool mbqi::quick_check(quantifier* q, quantifier* q_flat, q_body& qb) {
         unsigned_vector offsets;
         if (!first_offset(offsets, qb.vars))
             return false;
         var_subst subst(m);
+        expr_ref body(m);
         unsigned max_rounds = m_max_quick_check_rounds;
         unsigned num_bindings = 0;
         expr_ref_vector binding(m);
+        
         for (unsigned i = 0; i < max_rounds && num_bindings < m_max_cex; ++i) {
             set_binding(offsets, qb.vars, binding);
             if (m_model->is_true(qb.vbody)) {
-                expr_ref body = subst(q->get_expr(), binding);
+                body = subst(q_flat->get_expr(), binding);
                 if (is_forall(q))
                     body = ::mk_not(m, body);
                 add_instantiation(q, body);

src/sat/smt/q_mbi.h

@@ -96,7 +96,7 @@ namespace q {
         bool check_forall_default(quantifier* q, q_body& qb, model& mdl);
         bool check_forall_subst(quantifier* q, q_body& qb, model& mdl);
 
-        bool quick_check(quantifier* q, q_body& qb);
+        bool quick_check(quantifier* q, quantifier* q_flat, q_body& qb);
         bool next_offset(unsigned_vector& offsets, app_ref_vector const& vars);
         bool first_offset(unsigned_vector& offsets, app_ref_vector const& vars);
         bool next_offset(unsigned_vector& offsets, app_ref_vector const& vars, unsigned i, unsigned start);