** Calling: mathsat -input=smt2 -theory.fp.minmax_zero_mode=4 [GOOD] ; Automatically generated by SBV. Do not edit. [GOOD] (set-option :print-success true) [GOOD] (set-option :global-declarations true) [GOOD] (set-option :diagnostic-output-channel "stdout") [GOOD] (set-option :produce-interpolants true) [GOOD] (set-option :produce-models true) [GOOD] (set-logic ALL) ; has unbounded values, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () Int) ; tracks user variable "a" [GOOD] (declare-fun s1 () Int) ; tracks user variable "b" [GOOD] (declare-fun s2 () Int) ; tracks user variable "c" [GOOD] (declare-fun s3 () Int) ; tracks user variable "d" [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] ; --- arrays --- [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user given axioms --- [GOOD] ; --- formula --- [GOOD] (define-fun s4 () Bool (= s0 s1)) [GOOD] (define-fun s5 () Bool (= s0 s2)) [GOOD] (define-fun s6 () Bool (and s4 s5)) [GOOD] (define-fun s7 () Bool (= s1 s3)) [GOOD] (define-fun s8 () Bool (= s2 s3)) [GOOD] (define-fun s9 () Bool (not s8)) [GOOD] (define-fun s10 () Bool (and s7 s9)) [GOOD] (assert (! s6 :interpolation-group |c1|)) [GOOD] (assert (! s10 :interpolation-group |c2|)) [SEND] (check-sat) [RECV] unsat [SEND] (get-interpolant (|c1|)) [RECV] (= s1 s2) *** Solver : MathSAT *** Exit code: ExitSuccess FINAL OUTPUT: "(= s1 s2)"