mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

z3str3: disable compute_contains() and get_grounded_concats() checks

Browse source
This commit is contained in:
Murphy Berzish 2020-05-13 11:53:26 -04:00
parent 127ef59ce4
commit 3c606ea9b2
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_str.cpp
View file

@ -7626,9 +7626,11 @@ namespace smt {
var_eq_concat_map, var_eq_unroll_map, var_eq_concat_map, var_eq_unroll_map,
concat_eq_constStr_map, concat_eq_concat_map, unrollGroupMap);); concat_eq_constStr_map, concat_eq_concat_map, unrollGroupMap););
/*
if (!contain_pair_bool_map.empty()) { 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); compute_contains(aliasIndexMap, concats_eq_index_map, var_eq_constStr_map, concat_eq_constStr_map, var_eq_concat_map);
} }
*/
// step 4: dependence analysis // step 4: dependence analysis