mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

add round-off to farkas resconstruction in interp

Browse source
This commit is contained in:
Ken McMillan 2014-05-13 18:15:51 -07:00
parent c9e9b30af6
commit 95146483ea
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/interp/iz3translate.cpp
View file

@ -1364,8 +1364,13 @@ public:
int nprems = prems.size();
std::vector<ast> npcons(nprems);
hash_map<ast,ast> pain_map; // not needed
for(int i = 0; i < nprems; i++)
for(int i = 0; i < nprems; i++){
npcons[i] = painfully_normalize_ineq(conc(prems[i]),pain_map);
if(op(npcons[i]) == Lt){
ast constval = z3_simplify(make(Sub,arg(npcons[i],1),make_int(rational(1))));
npcons[i] = make(Leq,arg(npcons[i],0),constval);
}
}
ast ncon = painfully_normalize_ineq(mk_not(con),pain_map);
npcons.push_back(ncon);