From 2d8325ed43444fb0d65abd5f14d4eb1511fdaad6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Aug 2016 06:05:13 -0700 Subject: [PATCH] fix axiomatization of str.replace. Fixes issue #703 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 8b6c5baba..15122d7b6 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2902,9 +2902,11 @@ void theory_seq::add_replace_axiom(expr* r) { expr_ref xty = mk_concat(x, t, y); expr_ref xsy = mk_concat(x, s, y); literal cnt = mk_literal(m_util.str.mk_contains(a ,s)); + literal a_emp = mk_eq_empty(a); + add_axiom(~a_emp, mk_seq_eq(r, a)); add_axiom(cnt, mk_seq_eq(r, a)); - add_axiom(~cnt, mk_seq_eq(a, xsy)); - add_axiom(~cnt, mk_seq_eq(r, xty)); + add_axiom(~cnt, a_emp, mk_seq_eq(a, xsy)); + add_axiom(~cnt, a_emp, mk_seq_eq(r, xty)); tightest_prefix(s, x); }