From 218edbe9c68c7906971e1660510a6e7afe933ca6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Jun 2019 07:50:35 +0300 Subject: [PATCH] ensure also negative lt are constrained #2360 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 99e91f85e..0ee868c3a 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1242,7 +1242,7 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) { } br_status seq_rewriter::mk_str_le(expr* a, expr* b, expr_ref& result) { - result = m.mk_not(m_util.str.mk_lex_lt(b, a)); + result = m().mk_not(m_util.str.mk_lex_lt(b, a)); return BR_DONE; }