From 3c2fe497de4fee845f36e7a7bfc9b4860a6d265f Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 2 Aug 2016 16:44:54 -0400 Subject: [PATCH] modify theory_str::get_value() to check EQC for a numeral Instead of asking the arithmetic theory for the current assignment, we return the (unique) numeral in the equivalence class of the term whose length we want to know. This is because the arithmetic theory may return a default / internal value that doesn't correspond to anything actually asserted by the core solver. --- src/smt/theory_str.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 395e1dab6..2ae5dcec5 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -3832,13 +3832,13 @@ bool theory_str::get_value(expr* e, rational& val) const { enode * en_e = ctx.get_enode(e); enode * it = en_e; do { - if (tha->get_value(it, _val)) { + if (m_autil.is_numeral(it->get_owner(), val) && val.is_int()) { // found an arithmetic term - TRACE("t_str_int", tout << "get_value[" << mk_pp(it->get_owner(), m) << "] = " << mk_pp(_val, m) + TRACE("t_str_int", tout << mk_pp(it->get_owner(), m) << " is an integer ( ~= " << val << " )" << std::endl;); - return m_autil.is_numeral(_val, val) && val.is_int(); + return true; } else { - TRACE("t_str_int", tout << "get_value[" << mk_pp(it->get_owner(), m) << "] not found" << std::endl;); + TRACE("t_str_int", tout << mk_pp(it->get_owner(), m) << " not a numeral" << std::endl;); } it = it->get_next(); } while (it != en_e);