1** Calling: z3 -nw -in -smt2 2[GOOD] ; Automatically generated by SBV. Do not edit. 3[GOOD] (set-option :print-success true) 4[GOOD] (set-option :global-declarations true) 5[GOOD] (set-option :smtlib2_compliant true) 6[GOOD] (set-option :diagnostic-output-channel "stdout") 7[GOOD] (set-option :produce-models true) 8[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. 9[GOOD] ; --- uninterpreted sorts --- 10[GOOD] ; --- tuples --- 11[GOOD] ; --- sums --- 12[GOOD] ; --- literal constants --- 13[GOOD] ; --- skolem constants --- 14[GOOD] (declare-fun s0 () Int) ; tracks user variable "a" 15[GOOD] (declare-fun s1 () Int) ; tracks user variable "b" 16[GOOD] (declare-fun s2 () Int) ; tracks user variable "c" 17[GOOD] (declare-fun s3 () Int) ; tracks user variable "d" 18[GOOD] ; --- constant tables --- 19[GOOD] ; --- skolemized tables --- 20[GOOD] ; --- arrays --- 21[GOOD] ; --- uninterpreted constants --- 22[GOOD] ; --- user given axioms --- 23[GOOD] ; --- formula --- 24[GOOD] (define-fun s4 () Bool (= s0 s1)) 25[GOOD] (define-fun s5 () Bool (= s0 s2)) 26[GOOD] (define-fun s6 () Bool (and s4 s5)) 27[GOOD] (define-fun s7 () Bool (= s1 s3)) 28[GOOD] (define-fun s8 () Bool (= s2 s3)) 29[GOOD] (define-fun s9 () Bool (not s8)) 30[GOOD] (define-fun s10 () Bool (and s7 s9)) 31[SEND] (get-interpolant s6 s10) 32[RECV] (= s2 s1) 33*** Solver : Z3 34*** Exit code: ExitSuccess 35 36FINAL OUTPUT: 37"(= s2 s1)" 38