From d465938496acee3de07a5b27fada0b500b16c92c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Apr 2020 15:54:40 -0700 Subject: [PATCH] add lower bounds on lengths if they are not present Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index e3f20c6b4..3853e5f1f 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -549,7 +549,7 @@ bool theory_seq::branch_unit_variable() { break; } } - CTRACE("seq", result, tout << "branch unit variable";); + CTRACE("seq", result, tout << "branch unit variable\n";); return result; } @@ -5516,6 +5516,8 @@ bool theory_seq::get_length(expr* e, rational& val) { val += rational(s.length()); } else if (!has_length(c)) { + len = mk_len(c); + add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(0)))); TRACE("seq", tout << "literal has no length " << mk_pp(c, m) << "\n";); return false; }