mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge branch 'kenmcmil-issue204'
This commit is contained in:
commit
41c6f22130
|
@ -1082,8 +1082,10 @@ public:
|
|||
return best_coeff;
|
||||
}
|
||||
else
|
||||
if(op(t) != Numeral)
|
||||
if(op(t) != Numeral){
|
||||
v = get_linear_var(t);
|
||||
return(get_coeff(t));
|
||||
}
|
||||
return rational(0);
|
||||
}
|
||||
|
||||
|
@ -1092,10 +1094,10 @@ public:
|
|||
rational xcoeff = get_first_coefficient(arg(x,0),xvar);
|
||||
rational ycoeff = get_first_coefficient(arg(y,0),yvar);
|
||||
if(xcoeff == rational(0) || ycoeff == rational(0) || xvar != yvar)
|
||||
throw iz3_exception("bad assign-bounds lemma");
|
||||
throw unsupported(); // can be caused by non-linear arithmetic
|
||||
rational ratio = xcoeff/ycoeff;
|
||||
if(denominator(ratio) != rational(1))
|
||||
throw iz3_exception("bad assign-bounds lemma");
|
||||
throw unsupported(); // can this ever happen?
|
||||
return make_int(ratio); // better be integer!
|
||||
}
|
||||
|
||||
|
@ -1104,7 +1106,7 @@ public:
|
|||
get_assign_bounds_coeffs(proof,farkas_coeffs);
|
||||
int nargs = num_args(con);
|
||||
if(nargs != (int)(farkas_coeffs.size()))
|
||||
throw iz3_exception("bad assign-bounds theory lemma");
|
||||
throw unsupported(); // should never happen
|
||||
#if 0
|
||||
if(farkas_coeffs[0] != make_int(rational(1)))
|
||||
farkas_coeffs[0] = make_int(rational(1));
|
||||
|
|
Loading…
Reference in a new issue