From d6a2e7ac15bf3b931ee6d162db040958bafe47fc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 22 Mar 2020 13:21:48 -0700 Subject: [PATCH] fix #3433 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 1 - src/smt/theory_seq.cpp | 4 +++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 24157d428..5ba9504ed 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1824,7 +1824,6 @@ ast * ast_manager::register_node_core(ast * n) { } n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk(); - TRACE("ast", tout << "Object " << n->m_id << " was created.\n";); TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";); // increment reference counters diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index a62351edf..216b0f1d4 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1874,7 +1874,9 @@ bool theory_seq::propagate_length_coherence(expr* e) { elems.push_back(seq); tail = mk_concat(elems.size(), elems.c_ptr()); // len(e) >= low => e = tail; - literal low(mk_literal(m_autil.mk_ge(mk_len(e), m_autil.mk_numeral(lo, true)))); + expr_ref lo_e(m_autil.mk_numeral(lo, true), m); + expr_ref len_e_ge_lo(m_autil.mk_ge(mk_len(e), lo_e), m); + literal low = mk_literal(len_e_ge_lo); add_axiom(~low, mk_seq_eq(e, tail)); expr_ref len_e = mk_len(e); if (upper_bound(len_e, hi)) {