From 39fbf1e1742dfa88c63a0b236931af936277ad7f Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 2 Oct 2018 12:28:53 -0400
Subject: [PATCH] Z3str3: don't use arith_value::get_value in get_arith_value
---
src/smt/theory_str.cpp | 21 ++++++++++++++++++---
1 file changed, 18 insertions(+), 3 deletions(-)
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 662d76ae3..90bf171a0 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -4836,9 +4836,24 @@ namespace smt {
}
bool theory_str::get_arith_value(expr* e, rational& val) const {
- arith_value v(get_context());
- return v.get_value(e, val);
- }
+ context& ctx = get_context();
+ ast_manager & m = get_manager();
+ if (!ctx.e_internalized(e)) {
+ return false;
+ }
+ // check root of the eqc for an integer constant
+ // if an integer constant exists in the eqc, it should be the root
+ enode * en_e = ctx.get_enode(e);
+ enode * root_e = en_e->get_root();
+ if (m_autil.is_numeral(root_e->get_owner(), val) && val.is_int()) {
+ TRACE("str", tout << mk_pp(e, m) << " ~= " << mk_pp(root_e->get_owner(), m) << std::endl;);
+ return true;
+ } else {
+ TRACE("str", tout << "root of eqc of " << mk_pp(e, m) << " is not a numeral" << std::endl;);
+ return false;
+ }
+
+ }
bool theory_str::lower_bound(expr* _e, rational& lo) {
if (opt_DisableIntegerTheoryIntegration) {