From a59ee8032c0e6e7483f0b2bdad4b0dbe71ea4d1f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 13 Jun 2017 19:02:59 -0700
Subject: [PATCH] fix unsoundness bug in axiomatization of str.at. #1067
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/api/dotnet/FuncDecl.cs | 1 -
src/smt/smt_conflict_resolution.cpp | 4 +++-
src/smt/theory_seq.cpp | 4 ++--
3 files changed, 5 insertions(+), 4 deletions(-)
diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs
index 2f5cd0ce8..df90f9cd4 100644
--- a/src/api/dotnet/FuncDecl.cs
+++ b/src/api/dotnet/FuncDecl.cs
@@ -342,6 +342,5 @@ namespace Microsoft.Z3
Context.CheckContextMatch<Expr>(args);
return Expr.Create(Context, this, args);
}
-
}
}
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index 8d90f9583..ade667e34 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -1405,6 +1405,7 @@ namespace smt {
switch (js.get_kind()) {
case b_justification::CLAUSE: {
clause * cls = js.get_clause();
+ TRACE("unsat_core_bug", m_ctx.display_clause_detail(tout, cls););
unsigned num_lits = cls->get_num_literals();
unsigned i = 0;
if (consequent != false_literal) {
@@ -1422,8 +1423,9 @@ namespace smt {
process_antecedent_for_unsat_core(~l);
}
justification * js = cls->get_justification();
- if (js)
+ if (js) {
process_justification_for_unsat_core(js);
+ }
break;
}
case b_justification::BIN_CLAUSE:
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 3f8845546..af8b9e395 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3567,8 +3567,8 @@ void theory_seq::add_at_axiom(expr* e) {
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e, false));
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(i, len_x, false));
- add_axiom(i_ge_0, mk_eq(s, emp, false));
- add_axiom(~i_ge_len_s, mk_eq(s, emp, false));
+ add_axiom(i_ge_0, mk_eq(e, emp, false));
+ add_axiom(~i_ge_len_s, mk_eq(e, emp, false));
}
/**