mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

issue #204 -- throw better exception for non-linear arithmetic

Browse source
This commit is contained in:
Ken McMillan 2015-10-28 14:39:19 -07:00
parent 2d2ec38541
commit 8550de41a6
1 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/interp/iz3translate.cpp
View file

@ -1082,8 +1082,10 @@ public:
return best_coeff; return best_coeff;
} }
else else
if(op(t) != Numeral) if(op(t) != Numeral){
v = get_linear_var(t);
return(get_coeff(t)); return(get_coeff(t));
}
return rational(0); return rational(0);
} }
@ -1092,10 +1094,10 @@ public:
rational xcoeff = get_first_coefficient(arg(x,0),xvar); rational xcoeff = get_first_coefficient(arg(x,0),xvar);
rational ycoeff = get_first_coefficient(arg(y,0),yvar); rational ycoeff = get_first_coefficient(arg(y,0),yvar);
if(xcoeff == rational(0) || ycoeff == rational(0) || xvar != yvar) if(xcoeff == rational(0) || ycoeff == rational(0) || xvar != yvar)
throw "bad assign-bounds lemma"; throw unsupported(); // can be caused by non-linear arithmetic
rational ratio = xcoeff/ycoeff; rational ratio = xcoeff/ycoeff;
if(denominator(ratio) != rational(1)) if(denominator(ratio) != rational(1))
throw "bad assign-bounds lemma"; throw unsupported(); // can this ever happen?
return make_int(ratio); // better be integer! return make_int(ratio); // better be integer!
} }
@ -1104,7 +1106,7 @@ public:
get_assign_bounds_coeffs(proof,farkas_coeffs); get_assign_bounds_coeffs(proof,farkas_coeffs);
int nargs = num_args(con); int nargs = num_args(con);
if(nargs != (int)(farkas_coeffs.size())) if(nargs != (int)(farkas_coeffs.size()))
throw "bad assign-bounds theory lemma"; throw unsupported(); // should never happen
#if 0 #if 0
if(farkas_coeffs[0] != make_int(rational(1))) if(farkas_coeffs[0] != make_int(rational(1)))
farkas_coeffs[0] = make_int(rational(1)); farkas_coeffs[0] = make_int(rational(1));