From 86e7f83e061c2353b16021ca592335bf59f909ff Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 11 Jul 2017 13:24:48 -0400 Subject: [PATCH] proper theory_arith integration in theory_str::get_arith_value() --- src/smt/theory_str.cpp | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 2e928af37..bcb91b884 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -4664,7 +4664,19 @@ namespace smt { if (!tha) { return false; } - TRACE("str", tout << "checking eqc of " << mk_pp(e, m) << " for arithmetic value" << std::endl;); + + // first query theory_arith directly + + expr_ref ival(m); + if (ctx.e_internalized(e) && tha->get_value(ctx.get_enode(e), ival) + && m_autil.is_numeral(ival, val) && val.is_int()) { + TRACE("str", tout << "theory_arith: " << mk_pp(e, m) << " = " << val << std::endl;); + return true; + } + + // if this fails, fall back to checking eqc + + TRACE("str", tout << "no result in theory_arith! checking eqc of " << mk_pp(e, m) << " for arithmetic value" << std::endl;); expr_ref _val(m); enode * en_e = ctx.get_enode(e); enode * it = en_e;