From 47d33452c66064aae6148b342dc1e17a7315a34b Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 20 Mar 2015 17:39:45 -0700 Subject: [PATCH] interpolation fix (issue 182) --- src/interp/iz3interp.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index e1846d3b5..750c0c85e 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -97,6 +97,18 @@ struct frame_reducer : public iz3mgr { get_proof_assumptions_rec(proof,memo,used_frames); std::vector assertions_back_map(frames); + // if multiple children of a tree node are used, we can't delete it + std::vector 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++) if(used_frames[i] || i == z3_preds.size() - 1){ assertions.push_back(z3_preds[i]);