mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

interpolation fix (issue 182)

Browse source
This commit is contained in:
Ken McMillan 2015-03-20 17:39:45 -07:00
parent ece838bc80
commit 47d33452c6
1 changed files with 12 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/interp/iz3interp.cpp
View file

@ -97,6 +97,18 @@ struct frame_reducer : public iz3mgr {
get_proof_assumptions_rec(proof,memo,used_frames); get_proof_assumptions_rec(proof,memo,used_frames);
std::vector<int> assertions_back_map(frames); std::vector<int> assertions_back_map(frames);
// if multiple children of a tree node are used, we can't delete it
std::vector<int> used_children;
for(int i = 0; i < frames; i++)
used_children.push_back(0);
for(int i = 0; i < frames; i++)
if(orig_parents[i] != SHRT_MAX)
if(used_frames[i] || used_children[i]){
if(used_children[i] > 1)
used_frames[i] = true;
used_children[orig_parents[i]]++;
}
for(unsigned i = 0; i < z3_preds.size(); i++) for(unsigned i = 0; i < z3_preds.size(); i++)
if(used_frames[i] || i == z3_preds.size() - 1){ if(used_frames[i] || i == z3_preds.size() - 1){
assertions.push_back(z3_preds[i]); assertions.push_back(z3_preds[i]);