From 2075cb9fa4cef371a85845cf5a706897c3ecc0d4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Aug 2021 09:29:39 -0700 Subject: [PATCH] remove useless literal found during review #5470 --- src/ast/rewriter/seq_axioms.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 6458e36af..bcda71e54 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -1108,7 +1108,7 @@ namespace seq { expr_ref c = m_sk.mk("seq.prefix.c", s, t, char_sort); expr_ref d = m_sk.mk("seq.prefix.d", s, t, char_sort); add_clause(lit, s_gt_t, mk_seq_eq(s, mk_concat(x, seq.str.mk_unit(c), y))); - add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, seq.str.mk_unit(d), z)), mk_seq_eq(t, x)); + add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, seq.str.mk_unit(d), z))); add_clause(lit, s_gt_t, ~mk_eq(c, d)); #endif }