From 67d19cba4a2e28a8721bb3efa7539409d3486fa9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Mar 2020 14:13:12 -0700 Subject: [PATCH] fix #3105 fix #2937 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index fe47d4dac..94270ddb8 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -5704,12 +5704,12 @@ void theory_seq::add_at_axiom(expr* e) { expr_ref xey = mk_concat(x, e, y); expr_ref len_x = mk_len(x); add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, xey)); - 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(e, emp, false)); add_axiom(~i_ge_len_s, mk_eq(e, emp, false)); + add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e, false)); add_axiom(mk_literal(m_autil.mk_le(len_e, one))); }