From 894c60bdf90841c2af9c73897232027e9a94ead9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 19 Jun 2017 18:22:30 -0500
Subject: [PATCH] fix bug in qe-lite reported in #1086: bookkeeping of
unconstrained variables only works for quantifier-free formulas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/api/api_ast.cpp | 1 +
src/qe/qe_lite.cpp | 7 ++++++-
src/smt/theory_seq.cpp | 8 ++++++--
3 files changed, 13 insertions(+), 3 deletions(-)
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 7342b3c49..d34cad2f4 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -558,6 +558,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_sort(c, a);
RESET_ERROR_CODE();
+ CHECK_IS_EXPR(a, 0);
Z3_sort r = of_sort(mk_c(c)->m().get_sort(to_expr(a)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index eccc2d0c7..0e7db9971 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -1491,8 +1491,10 @@ namespace fm {
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
expr * f = g[i];
- if (is_occ(f))
+ if (is_occ(f)) {
+ TRACE("qe_lite", tout << "OCC: " << mk_ismt2_pp(f, m) << "\n";);
continue;
+ }
TRACE("qe_lite", tout << "not OCC:\n" << mk_ismt2_pp(f, m) << "\n";);
quick_for_each_expr(proc, visited, f);
}
@@ -2221,6 +2223,9 @@ namespace fm {
void operator()(expr_ref_vector& fmls) {
init(fmls);
init_use_list(fmls);
+ for (auto & f : fmls) {
+ if (has_quantifiers(f)) return;
+ }
if (m_inconsistent) {
m_new_fmls.reset();
m_new_fmls.push_back(m.mk_false());
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index c98040c17..3b70e1426 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2180,8 +2180,12 @@ void theory_seq::internalize_eq_eh(app * atom, bool_var v) {
}
bool theory_seq::internalize_atom(app* a, bool) {
- return internalize_term(a);
#if 0
+ return internalize_term(a);
+#else
+ if (is_skolem(m_eq, a)) {
+ return internalize_term(a);
+ }
context & ctx = get_context();
bool_var bv = ctx.mk_bool_var(a);
ctx.set_var_theory(bv, get_id());
@@ -2196,7 +2200,7 @@ bool theory_seq::internalize_atom(app* a, bool) {
m_util.str.is_suffix(a, e1, e2)) {
return internalize_term(to_app(e1)) && internalize_term(to_app(e2));
}
- if (is_accept(a) || is_reject(a) || is_skolem(m_eq, a) || is_step(a) || is_skolem(symbol("seq.is_digit"), a)) {
+ if (is_accept(a) || is_reject(a) || is_step(a) || is_skolem(symbol("seq.is_digit"), a)) {
return true;
}
UNREACHABLE();