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

issue #48 disabled rounding for strict real inequalities

Browse source
This commit is contained in:
Ken McMillan 2015-07-10 11:00:13 -07:00
parent ade9b2830a
commit 1cf24f7cdc
2 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/interp/iz3mgr.cpp
View file

@ -733,6 +733,8 @@ void iz3mgr::linear_comb(ast &P, const ast &c, const ast &Q, bool round_off){
} }
} }
bool pstrict = op(P) == Lt; bool pstrict = op(P) == Lt;
if (round_off && get_type(Qrhs) != int_type())
round_off = false;
if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){ if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){
Qrhs = make(Sub,Qrhs,make_int(rational(1))); Qrhs = make(Sub,Qrhs,make_int(rational(1)));
qstrict = false; qstrict = false;

2
src/interp/iz3proof_itp.cpp
View file

@ -2584,6 +2584,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
if(pstrict && qstrict && round_off) if(pstrict && qstrict && round_off)
Qrhs = make(Sub,Qrhs,make_int(rational(1))); Qrhs = make(Sub,Qrhs,make_int(rational(1)));
#else #else
if (round_off && get_type(Qrhs) != int_type())
round_off = false;
bool pstrict = op(P) == Lt; bool pstrict = op(P) == Lt;
if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){ if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){
Qrhs = make(Sub,Qrhs,make_int(rational(1))); Qrhs = make(Sub,Qrhs,make_int(rational(1)));