mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix for tree interpolation

Browse source
This commit is contained in:
Ken McMillan 2014-08-05 11:11:43 -07:00
parent aa35149700
commit 7bf87e76ea
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/interp/iz3interp.cpp
View file

@ -347,8 +347,10 @@ public:
// get the interps for the tree positions // get the interps for the tree positions
std::vector<ast> _interps = interps; std::vector<ast> _interps = interps;
interps.resize(pos_map.size()); interps.resize(pos_map.size());
for(unsigned i = 0; i < pos_map.size(); i++) for(unsigned i = 0; i < pos_map.size(); i++){
interps[i] = i < _interps.size() ? _interps[i] : mk_false(); unsigned j = pos_map[i];
interps[i] = j < _interps.size() ? _interps[j] : mk_false();
}
} }
bool has_interp(hash_map<ast,bool> &memo, const ast &t){ bool has_interp(hash_map<ast,bool> &memo, const ast &t){