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

interpolation fix

Browse source
This commit is contained in:
Ken McMillan 2013-11-06 12:20:55 -08:00
parent 0696a7ef50
commit 33f941aaec
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/interp/iz3mgr.cpp
View file

@ -594,6 +594,7 @@ void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector<rationa
} }
rats[i-1] = r; rats[i-1] = r;
} }
#if 0
if(rats[1].is_neg()){ // work around bug -- if all coeffs negative, negate them if(rats[1].is_neg()){ // work around bug -- if all coeffs negative, negate them
for(unsigned i = 1; i < rats.size(); i++){ for(unsigned i = 1; i < rats.size(); i++){
if(!rats[i].is_neg()) if(!rats[i].is_neg())
@ -601,6 +602,8 @@ void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector<rationa
rats[i] = -rats[i]; rats[i] = -rats[i];
} }
} }
#endif
abs_rat(rats);
extract_lcd(rats); extract_lcd(rats);
} }