mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

interpolation fix

Browse source
This commit is contained in:
Ken McMillan 2014-02-28 10:38:35 -08:00
parent 08d892bbdb
commit 19dbd02e13
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/interp/iz3proof_itp.cpp
View file

@ -2635,6 +2635,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
} }
hash_map<ast,ast>::iterator it = localization_map.find(e); hash_map<ast,ast>::iterator it = localization_map.find(e);
if(it != localization_map.end() && is_bool_type(get_type(e))
&& !pv->ranges_intersect(pv->ast_scope(it->second),rng))
it = localization_map.end(); // prevent quantifiers over booleans
if(it != localization_map.end()){ if(it != localization_map.end()){
pf = localization_pf_map[e]; pf = localization_pf_map[e];
e = it->second; e = it->second;