From 8550de41a6f3a3ada23aa8f550af3e5dcca46afc Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 28 Oct 2015 14:39:19 -0700 Subject: [PATCH] issue #204 -- throw better exception for non-linear arithmetic --- src/interp/iz3translate.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 51084f809..8e69f28d7 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -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 "bad assign-bounds lemma"; + throw unsupported(); // can be caused by non-linear arithmetic rational ratio = xcoeff/ycoeff; if(denominator(ratio) != rational(1)) - throw "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 "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));