mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

Gracefully failing in assign-bounds to farkas

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-24 21:03:09 -04:00
parent e906930922
commit f330b96a35
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/muz/spacer/spacer_proof_utils.cpp
View file

@ -307,7 +307,10 @@ namespace spacer {
rational rat1, rat2, coeff0;
arith_util a(m);
if (a.is_numeral(val1, rat1) && a.is_numeral(val2, rat2)) {
CTRACE("spacer.fkab", !(val1 && val2),
tout << "Failed to match variables\n";);
if (val1 && val2 &&
a.is_numeral(val1, rat1) && a.is_numeral(val2, rat2)) {
coeff0 = abs(rat2/rat1);
coeff0 = coeff0 / lcb.lc();
TRACE("spacer.fkab", tout << "coeff0: " << coeff0 << "\n";);