From b3fddf47076faa65964735c5c64963dfe202af11 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 12 Sep 2016 16:41:35 -0400 Subject: [PATCH] performance optimization in theory_str::classify_ast_by_type --- src/smt/theory_str.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 511585fa8..ecc3b7247 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -6597,10 +6597,10 @@ void theory_str::classify_ast_by_type(expr * node, std::map & varMap expr * arg1Val = get_eqc_value(arg1, arg1HasEq); int canskip = 0; - if (arg0HasEq && arg0Val == m_strutil.mk_string("")) { + if (arg0HasEq && m_strutil.get_string_constant_value(arg0Val).empty()) { canskip = 1; } - if (canskip == 0 && arg1HasEq && arg1Val == m_strutil.mk_string("")) { + if (canskip == 0 && arg1HasEq && m_strutil.get_string_constant_value(arg1Val).empty()) { canskip = 1; } if (canskip == 0 && concatMap.find(node) == concatMap.end()) {