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