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 BV) 9[GOOD] ; --- uninterpreted sorts --- 10[GOOD] ; --- tuples --- 11[GOOD] ; --- sums --- 12[GOOD] ; --- literal constants --- 13[GOOD] ; --- skolem constants --- 14[GOOD] ; --- constant tables --- 15[GOOD] ; --- skolemized tables --- 16[GOOD] ; --- arrays --- 17[GOOD] ; --- uninterpreted constants --- 18[GOOD] ; --- user given axioms --- 19[GOOD] ; --- formula --- 20[GOOD] (assert (forall ((s0 (_ BitVec 8)) 21 (s1 (_ BitVec 8))) 22 (let ((s2 (= s0 s1))) 23 (let ((s3 (distinct s0 s1))) 24 (let ((s4 (and s2 s3))) 25 (not s4)))))) 26[SEND] (check-sat) 27[RECV] sat 28*** In a quantified context, obvservables will not be printed. 29*** Solver : Z3 30*** Exit code: ExitSuccess 31