mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix unsoundness bug in axiomatization of str.at. #1067

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-13 19:02:59 -07:00
parent 6bce173248
commit a59ee8032c
3 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/api/dotnet/FuncDecl.cs
View file

@ -342,6 +342,5 @@ namespace Microsoft.Z3
Context.CheckContextMatch<Expr>(args); Context.CheckContextMatch<Expr>(args);
return Expr.Create(Context, this, args); return Expr.Create(Context, this, args);
} }
} }
} }

4
src/smt/smt_conflict_resolution.cpp
View file

@ -1405,6 +1405,7 @@ namespace smt {
switch (js.get_kind()) { switch (js.get_kind()) {
case b_justification::CLAUSE: { case b_justification::CLAUSE: {
clause * cls = js.get_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 num_lits = cls->get_num_literals();
unsigned i = 0; unsigned i = 0;
if (consequent != false_literal) { if (consequent != false_literal) {
@ -1422,8 +1423,9 @@ namespace smt {
process_antecedent_for_unsat_core(~l); process_antecedent_for_unsat_core(~l);
} }
justification * js = cls->get_justification(); justification * js = cls->get_justification();
if (js) if (js) {
process_justification_for_unsat_core(js); process_justification_for_unsat_core(js);
}
break; break;
} }
case b_justification::BIN_CLAUSE: case b_justification::BIN_CLAUSE:

4
src/smt/theory_seq.cpp
View file

@ -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(one, len_e, false));
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(i, len_x, 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_0, mk_eq(e, emp, false));
add_axiom(~i_ge_len_s, mk_eq(s, emp, false)); add_axiom(~i_ge_len_s, mk_eq(e, emp, false));
} }
/** /**