iZ3 - wrong interpolant from Farkas proof

[agriggio]

Z3 computes a wrong interpolant for the example below.

I think this is due to the "rounding off" done in order to deal with
integer inequalities, which is performed regardless of whether the input
inequality is over the integer or over the rationals.

I'm also attaching a tentative patch for the issue.

Here's an SMT-LIB2 example showing the problem:

(set-logic QF_LRA)

(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)

(define-fun A () Bool
  (and
   (not (<= x 0.0))
   (>= (+ (* 10.0 y) (* (- 9.0) x)) 0.0)
   )
  )

(define-fun B () Bool
  (and (>= z 0.0)
       (<= (+ (* 10.0 y) (* 9.0 z)) 0.0))
  )

(compute-interpolant (and (interp A) B))
(exit)

;; computed wrong interpolant:
(define-fun I () Bool
  (>= y (/ 9.0 10.0)))
;; a correct interpolant is: (not (<= y 0.0))

(assert (or (and A (not I)) (and B I)))
(check-sat)

Here's a tentative patch:

diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp
--- a/src/interp/iz3proof_itp.cpp
+++ b/src/interp/iz3proof_itp.cpp
@@ -2590,6 +2590,9 @@
         if(pstrict && qstrict && round_off)
             Qrhs = make(Sub,Qrhs,make_int(rational(1)));
 #else
+        if (round_off && get_type(Qrhs) != int_type()) {
+            round_off = false;
+        }
         bool pstrict = op(P) == Lt;
         if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){
             Qrhs = make(Sub,Qrhs,make_int(rational(1)));

[kenmcmil]

Interpolation doesn't actually support reals. Just the theory AUFLIA. I suspect there are several places it needs to be patched for real support. Thanks for sending the patch, though.

[wintersteiger]

Ken, could you add a check so we get better error messages for this and similar cases? We have existing probes for QF_AUFLIA in probe_arith.h/.cpp

[kenmcmil]

I fixed this problem (wrong interpolant) by preventing rounding of real inequalities in a couple of places. The question of how to give a better error message when interpolation fails is still open. Closing this issue, however.