From 3c606ea9b206bb08df62855c2c1f14cccebdd1fb Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 13 May 2020 11:53:26 -0400 Subject: [PATCH] z3str3: disable compute_contains() and get_grounded_concats() checks --- src/smt/theory_str.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index c9904996e..ab67fc2f7 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -7626,9 +7626,11 @@ namespace smt { var_eq_concat_map, var_eq_unroll_map, concat_eq_constStr_map, concat_eq_concat_map, unrollGroupMap);); + /* if (!contain_pair_bool_map.empty()) { compute_contains(aliasIndexMap, concats_eq_index_map, var_eq_constStr_map, concat_eq_constStr_map, var_eq_concat_map); } + */ // step 4: dependence analysis