From e9411e5b8c6d80de3f8866071ae89cc4f7df431c Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 9 Dec 2016 17:12:29 -0500 Subject: [PATCH] explicitly re-introduce string axioms on refreshed string theory vars this fixes at least one case (kaluza/unsat/big/9650.smt2) where a string could have a negative length value due to a constraint that went out of scope --- src/smt/theory_str.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 92920c220..a6d93e70b 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -320,6 +320,9 @@ void theory_str::refresh_theory_var(expr * e) { enode * en = ensure_enode(e); theory_var v = mk_var(en); TRACE("t_str_detail", tout << "refresh " << mk_pp(e, get_manager()) << ": v#" << v << std::endl;); + // TODO this is probably sub-optimal + // TODO case where the refreshed var must be non-empty? + m_basicstr_axiom_todo.push_back(en); } theory_var theory_str::mk_var(enode* n) {