LIA interpolation produces different results in Debug and Release modes

[BritikovKI]

For certain SMT problems interpolation seems to produce different outputs for the interpolation.
Particularly, for the following interpolation construction:
A: (or (and (= 1 (+ |x#3##0| (* -1 |x#3##1|))) (= 0 (+ |x#2##0| (* -1 |x#2##1|))) (<= 0 |x#3##1|)) (and (= 0 (+ |x#2##1| (* -1 |x#3##1|))) (= 1 (+ |x#2##0| (* -1 |x#3##1|))) (<= 0 (* -1 |x#3##0|)) (<= 1 |x#3##1|)))

B: (and (not (or (not (or (and (not (<= 1 |x#3##1|)) (<= 0 (* -1 |x#3##1|)) (<= 2 |x#2##1|)) (and (<= 1 |x#3##1|) (not (<= 0 (* -1 |x#3##1|))) (<= 1 (+ (* -1 |x#2##1|) |x#3##1|)) (not (<= 3 |x#3##1|))) (and (not (<= 0 (+ |x#2##1| (* -1 |x#3##1|)))) (not (<= 0 (* -1 |x#3##1|))) (<= 2 |x#2##1|) (<= 3 |x#3##1|) (<= -2 (* -1 |x#2##1|)) (<= -2 (+ |x#2##1| (* -1 |x#3##1|)))) (and (<= 1 |x#3##1|) (not (<= 0 (* -1 |x#3##1|))) (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (and (not (<= 0 (+ |x#2##1| (* -1 |x#3##1|)))) (not (<= 0 (* -1 |x#3##1|))) (<= 2 |x#2##1|) (<= 1 (+ (* -1 |x#2##1|) |x#3##1|)) (<= -2 (+ |x#2##1| (* -1 |x#3##1|)))) (and (<= 1 |x#2##1|) (not (<= 0 (+ |x#2##1| (* -1 |x#3##1|)))) (not (<= 0 (* -1 |x#3##1|))) (<= 3 |x#3##1|) (<= 2 (+ (* -1 |x#2##1|) |x#3##1|))))) (and (<= 1 |x#3##1|) (<= -1 (* -1 |x#3##1|)) (= (+ |x#2##1| (* -1 |x#3##1|)) 4) (or (and (<= 0 (+ |x#2##1| (* -1 |x#3##1|))) (not (<= 0 (* -1 |x#3##1|))) (<= 2 |x#3##1|) (not (<= 1 (+ (* -1 |x#2##1|) |x#3##1|))) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (<= -2 (+ |x#2##1| (* |x#3##1| -2))) (<= 1 (+ (* -1 |x#2##1|) (* |x#3##1| 2)))) (and (not (<= 0 (* -1 |x#3##1|))) (<= 2 |x#2##1|) (<= 1 (+ (* -1 |x#2##1|) |x#3##1|)) (<= 3 |x#3##1|) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (not (<= 2 (+ (* -1 |x#2##1|) |x#3##1|))) (<= -1 (+ |x#2##1| (* -1 |x#3##1|)))) (and (not (<= 0 (* -1 |x#3##1|))) (<= 2 |x#2##1|) (<= 3 |x#3##1|) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (<= -2 (* -1 |x#2##1|))) (and (<= 1 |x#2##1|) (not (<= 0 (* -1 |x#3##1|))) (not (<= 2 |x#2##1|)) (<= 1 (+ (* -1 |x#2##1|) |x#3##1|)) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (<= -2 (+ |x#2##1| (* -1 |x#3##1|))) (not (<= 2 (+ (* -1 |x#2##1|) |x#3##1|)))) (and (not (<= 0 (+ |x#2##1| (* -1 |x#3##1|)))) (not (<= 0 (* -1 |x#3##1|))) (<= 3 |x#3##1|) (<= 2 (+ (* -1 |x#2##1|) |x#3##1|)) (<= 3 |x#2##1|)) (and (not (<= 1 |x#2##1|)) (not (<= 0 (* -1 |x#3##1|))) (<= 3 |x#3##1|) (<= -3 (* -1 |x#3##1|)) (<= 1 (* -1 |x#2##1|))) (and (<= 0 (+ |x#2##1| (* -1 |x#3##1|))) (not (<= 0 (* -1 |x#3##1|))) (<= 3 |x#3##1|) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|))))) (and (not (<= 0 (* -1 |x#3##1|))) (not (<= 2 |x#2##1|)) (<= -4 (+ |x#2##1| (* -1 |x#3##1|))) (<= 4 (+ (* -1 |x#2##1|) |x#3##1|)) (<= -1 |x#2##1|)) (and (not (<= 1 |x#2##1|)) (not (<= 0 (* -1 |x#3##1|))) (<= 3 |x#3##1|) (<= 4 (+ (* -1 |x#2##1|) |x#3##1|))) (and (not (<= 0 (* -1 |x#3##1|))) (not (<= 2 |x#2##1|)) (<= 3 |x#3##1|) (<= 4 (+ (* -1 |x#2##1|) |x#3##1|))) (and (<= 1 |x#2##1|) (not (<= 0 (* -1 |x#3##1|))) (not (<= 2 |x#2##1|)) (<= 1 (+ (* -1 |x#2##1|) |x#3##1|)) (<= 3 |x#3##1|) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (<= -2 (+ |x#2##1| (* -1 |x#3##1|)))) (and (not (<= 1 |x#2##1|)) (not (<= 0 (* -1 |x#3##1|))) (<= 1 (+ (* -1 |x#2##1|) |x#3##1|)) (<= 3 |x#3##1|) (<= -3 (* -1 |x#3##1|)) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (<= 0 (* -1 |x#2##1|))) (and (not (<= 0 (* -1 |x#3##1|))) (not (<= 2 |x#2##1|)) (<= 3 |x#3##1|) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (<= 2 (+ (* -1 |x#2##1|) |x#3##1|))) (and (not (<= 0 (* -1 |x#3##1|))) (not (<= 1 (+ (* -1 |x#2##1|) |x#3##1|))) (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (and (not (<= 1 |x#2##1|)) (not (<= 0 (* -1 |x#3##1|))) (<= 1 (+ (* -1 |x#2##1|) |x#3##1|)) (not (<= 3 |x#3##1|)) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|))))) (and (not (<= 0 (* -1 |x#3##1|))) (<= 1 (+ |x#2##1| (* -1 |x#3##1|))) (not (<= 1 (+ (* -1 |x#2##1|) |x#3##1|))) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (<= 0 (+ (* -1 |x#2##1|) (* |x#3##1| 2))) (<= 0 (+ |x#2##1| (* |x#3##1| -2)))))))) (not (or (and (<= 2 |x#2##0|) (<= 1 |x#3##0|) (<= -1 (* -1 |x#3##0|))) (and (<= 1 (+ |x#2##0| (* -1 |x#3##0|))) (<= 3 |x#3##0|)) (and (<= 2 |x#2##0|) (<= -2 (* -1 |x#2##0|)) (<= 2 (+ (* -1 |x#2##0|) |x#3##0|)) (<= 4 |x#3##0|) (<= -3 (+ |x#2##0| (* -1 |x#3##0|)))) (and (<= 2 |x#3##0|) (<= 1 (+ |x#2##0| (* -1 |x#3##0|))) (<= -2 (+ (* -1 |x#2##0|) |x#3##0|))) (and (<= 2 (+ (* -1 |x#2##0|) |x#3##0|)) (<= 3 |x#3##0|) (<= -3 (* -1 |x#3##0|))) (and (<= 2 |x#3##0|) (<= 4 (+ |x#2##0| (* -1 |x#3##0|)))) (and (<= 2 |x#3##0|) (<= 2 (+ (* -1 |x#2##0|) |x#3##0|)) (<= -3 (* -1 |x#3##0|))) (and (<= 1 |x#2##0|) (<= 4 |x#3##0|) (<= 3 (+ (* -1 |x#2##0|) |x#3##0|))) (and (<= 2 |x#2##0|) (<= 2 (+ (* -1 |x#2##0|) |x#3##0|)) (<= 3 |x#3##0|) (<= -3 (+ |x#2##0| (* -1 |x#3##0|)))))))

getInterpolationContext returns different interpolants.

[blishko]

I think you have to be a bit more specific.
I have tried to reproduce this with the following script:

(set-option :produce-interpolants true)
(set-logic QF_LIA)

; Variable declarations
(declare-fun |x#2##0| () Int)
(declare-fun |x#2##1| () Int)
(declare-fun |x#3##0| () Int)
(declare-fun |x#3##1| () Int)

; First formula
(assert (!
  (or
    (and (= 1 (+ |x#3##0| (* -1 |x#3##1|)))
         (= 0 (+ |x#2##0| (* -1 |x#2##1|)))
         (<= 0 |x#3##1|))
    (and (= 0 (+ |x#2##1| (* -1 |x#3##1|)))
         (= 1 (+ |x#2##0| (* -1 |x#3##1|)))
         (<= 0 (* -1 |x#3##0|))
         (<= 1 |x#3##1|))
  )
 :named A))

; Second formula
(assert (!
(and
 (not
  (or
   (not
    (or
     (and (not (<= 1 |x#3##1|)) (<= 0 (* -1 |x#3##1|)) (<= 2 |x#2##1|))
     (and (<= 1 |x#3##1|) (not (<= 0 (* -1 |x#3##1|))) (<= 1 (+ (* -1 |x#2##1|) |x#3##1|)) (not (<= 3 |x#3##1|)))
     (and (not (<= 0 (+ |x#2##1| (* -1 |x#3##1|)))) (not (<= 0 (* -1 |x#3##1|))) (<= 2 |x#2##1|) (<= 3 |x#3##1|) (<= -2 (* -1 |x#2##1|)) (<= -2 (+ |x#2##1| (* -1 |x#3##1|))))
     (and (<= 1 |x#3##1|) (not (<= 0 (* -1 |x#3##1|))) (<= 2 (+ |x#2##1| (* -1 |x#3##1|))))
     (and (not (<= 0 (+ |x#2##1| (* -1 |x#3##1|)))) (not (<= 0 (* -1 |x#3##1|))) (<= 2 |x#2##1|) (<= 1 (+ (* -1 |x#2##1|) |x#3##1|)) (<= -2 (+ |x#2##1| (* -1 |x#3##1|))))
     (and (<= 1 |x#2##1|) (not (<= 0 (+ |x#2##1| (* -1 |x#3##1|)))) (not (<= 0 (* -1 |x#3##1|))) (<= 3 |x#3##1|) (<= 2 (+ (* -1 |x#2##1|) |x#3##1|)))
    )
   )
   (and
    (<= 1 |x#3##1|)
    (<= -1 (* -1 |x#3##1|))
    (= (+ |x#2##1| (* -1 |x#3##1|)) 4)
    (or
     (and (<= 0 (+ |x#2##1| (* -1 |x#3##1|))) (not (<= 0 (* -1 |x#3##1|))) (<= 2 |x#3##1|) (not (<= 1 (+ (* -1 |x#2##1|) |x#3##1|))) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (<= -2 (+ |x#2##1| (* |x#3##1| -2))) (<= 1 (+ (* -1 |x#2##1|) (* |x#3##1| 2))))
     (and (not (<= 0 (* -1 |x#3##1|))) (<= 2 |x#2##1|) (<= 1 (+ (* -1 |x#2##1|) |x#3##1|)) (<= 3 |x#3##1|) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (not (<= 2 (+ (* -1 |x#2##1|) |x#3##1|))) (<= -1 (+ |x#2##1| (* -1 |x#3##1|))))
     (and (not (<= 0 (* -1 |x#3##1|))) (<= 2 |x#2##1|) (<= 3 |x#3##1|) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (<= -2 (* -1 |x#2##1|)))
     (and (<= 1 |x#2##1|) (not (<= 0 (* -1 |x#3##1|))) (not (<= 2 |x#2##1|)) (<= 1 (+ (* -1 |x#2##1|) |x#3##1|)) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (<= -2 (+ |x#2##1| (* -1 |x#3##1|))) (not (<= 2 (+ (* -1 |x#2##1|) |x#3##1|))))
     (and (not (<= 0 (+ |x#2##1| (* -1 |x#3##1|)))) (not (<= 0 (* -1 |x#3##1|))) (<= 3 |x#3##1|) (<= 2 (+ (* -1 |x#2##1|) |x#3##1|)) (<= 3 |x#2##1|))
     (and (not (<= 1 |x#2##1|)) (not (<= 0 (* -1 |x#3##1|))) (<= 3 |x#3##1|) (<= -3 (* -1 |x#3##1|)) (<= 1 (* -1 |x#2##1|)))
     (and (<= 0 (+ |x#2##1| (* -1 |x#3##1|))) (not (<= 0 (* -1 |x#3##1|))) (<= 3 |x#3##1|) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))))
     (and (not (<= 0 (* -1 |x#3##1|))) (not (<= 2 |x#2##1|)) (<= -4 (+ |x#2##1| (* -1 |x#3##1|))) (<= 4 (+ (* -1 |x#2##1|) |x#3##1|)) (<= -1 |x#2##1|))
     (and (not (<= 1 |x#2##1|)) (not (<= 0 (* -1 |x#3##1|))) (<= 3 |x#3##1|) (<= 4 (+ (* -1 |x#2##1|) |x#3##1|)))
     (and (not (<= 0 (* -1 |x#3##1|))) (not (<= 2 |x#2##1|)) (<= 3 |x#3##1|) (<= 4 (+ (* -1 |x#2##1|) |x#3##1|)))
     (and (<= 1 |x#2##1|) (not (<= 0 (* -1 |x#3##1|))) (not (<= 2 |x#2##1|)) (<= 1 (+ (* -1 |x#2##1|) |x#3##1|)) (<= 3 |x#3##1|) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (<= -2 (+ |x#2##1| (* -1 |x#3##1|))))
     (and (not (<= 1 |x#2##1|)) (not (<= 0 (* -1 |x#3##1|))) (<= 1 (+ (* -1 |x#2##1|) |x#3##1|)) (<= 3 |x#3##1|) (<= -3 (* -1 |x#3##1|)) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (<= 0 (* -1 |x#2##1|)))
     (and (not (<= 0 (* -1 |x#3##1|))) (not (<= 2 |x#2##1|)) (<= 3 |x#3##1|) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (<= 2 (+ (* -1 |x#2##1|) |x#3##1|)))
     (and (not (<= 0 (* -1 |x#3##1|))) (not (<= 1 (+ (* -1 |x#2##1|) |x#3##1|))) (<= 2 (+ |x#2##1| (* -1 |x#3##1|))))
     (and (not (<= 1 |x#2##1|)) (not (<= 0 (* -1 |x#3##1|))) (<= 1 (+ (* -1 |x#2##1|) |x#3##1|)) (not (<= 3 |x#3##1|)) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))))
     (and (not (<= 0 (* -1 |x#3##1|))) (<= 1 (+ |x#2##1| (* -1 |x#3##1|))) (not (<= 1 (+ (* -1 |x#2##1|) |x#3##1|))) (not (<= 2 (+ |x#2##1| (* -1 |x#3##1|)))) (<= 0 (+ (* -1 |x#2##1|) (* |x#3##1| 2))) (<= 0 (+ |x#2##1| (* |x#3##1| -2))))
    )
   )
  )
 )
 (not
  (or
   (and (<= 2 |x#2##0|) (<= 1 |x#3##0|) (<= -1 (* -1 |x#3##0|)))
   (and (<= 1 (+ |x#2##0| (* -1 |x#3##0|))) (<= 3 |x#3##0|))
   (and (<= 2 |x#2##0|) (<= -2 (* -1 |x#2##0|)) (<= 2 (+ (* -1 |x#2##0|) |x#3##0|)) (<= 4 |x#3##0|) (<= -3 (+ |x#2##0| (* -1 |x#3##0|))))
   (and (<= 2 |x#3##0|) (<= 1 (+ |x#2##0| (* -1 |x#3##0|))) (<= -2 (+ (* -1 |x#2##0|) |x#3##0|)))
   (and (<= 2 (+ (* -1 |x#2##0|) |x#3##0|)) (<= 3 |x#3##0|) (<= -3 (* -1 |x#3##0|)))
   (and (<= 2 |x#3##0|) (<= 4 (+ |x#2##0| (* -1 |x#3##0|))))
   (and (<= 2 |x#3##0|) (<= 2 (+ (* -1 |x#2##0|) |x#3##0|)) (<= -3 (* -1 |x#3##0|)))
   (and (<= 1 |x#2##0|) (<= 4 |x#3##0|) (<= 3 (+ (* -1 |x#2##0|) |x#3##0|)))
   (and (<= 2 |x#2##0|) (<= 2 (+ (* -1 |x#2##0|) |x#3##0|)) (<= 3 |x#3##0|) (<= -3 (+ |x#2##0| (* -1 |x#3##0|))))
  )
 )) :named B))

(check-sat)
(get-interpolants A B)

But I get the same interpolant in debug and release build.
Any options you are setting for the interpolantion procedure?