** Calling: cvc4 --lang smt --incremental --interactive --no-interactive-prompt [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-models true) [GOOD] (set-logic QF_UFBV) [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] (define-fun s2 () (_ BitVec 8) #x20) [GOOD] (define-fun s5 () (_ BitVec 1) #b0) [GOOD] (define-fun s55 () (_ BitVec 32) #x00000000) [GOOD] ; --- skolem constants --- [GOOD] (declare-fun s0 () (_ BitVec 32)) [GOOD] (declare-fun s1 () (_ BitVec 8)) [GOOD] ; --- constant tables --- [GOOD] ; --- skolemized tables --- [GOOD] (declare-fun table0 ((_ BitVec 8)) (_ BitVec 32)) [GOOD] ; --- arrays --- [GOOD] ; --- uninterpreted constants --- [GOOD] ; --- user given axioms --- [GOOD] ; --- formula --- [GOOD] (define-fun s3 () (_ BitVec 8) (bvurem s1 s2)) [GOOD] (define-fun s4 () (_ BitVec 1) ((_ extract 4 4) s3)) [GOOD] (define-fun s6 () Bool (distinct s4 s5)) [GOOD] (define-fun s7 () (_ BitVec 1) ((_ extract 3 3) s3)) [GOOD] (define-fun s8 () Bool (distinct s5 s7)) [GOOD] (define-fun s9 () (_ BitVec 1) ((_ extract 2 2) s3)) [GOOD] (define-fun s10 () Bool (distinct s5 s9)) [GOOD] (define-fun s11 () (_ BitVec 1) ((_ extract 1 1) s3)) [GOOD] (define-fun s12 () Bool (distinct s5 s11)) [GOOD] (define-fun s13 () (_ BitVec 1) ((_ extract 0 0) s3)) [GOOD] (define-fun s14 () Bool (distinct s5 s13)) [GOOD] (define-fun s15 () (_ BitVec 32) ((_ rotate_left 1) s0)) [GOOD] (define-fun s16 () (_ BitVec 32) (ite s14 s15 s0)) [GOOD] (define-fun s17 () (_ BitVec 32) ((_ rotate_left 2) s16)) [GOOD] (define-fun s18 () (_ BitVec 32) (ite s12 s17 s16)) [GOOD] (define-fun s19 () (_ BitVec 32) ((_ rotate_left 4) s18)) [GOOD] (define-fun s20 () (_ BitVec 32) (ite s10 s19 s18)) [GOOD] (define-fun s21 () (_ BitVec 32) ((_ rotate_left 8) s20)) [GOOD] (define-fun s22 () (_ BitVec 32) (ite s8 s21 s20)) [GOOD] (define-fun s23 () (_ BitVec 32) ((_ rotate_left 16) s22)) [GOOD] (define-fun s24 () (_ BitVec 32) (ite s6 s23 s22)) [GOOD] (define-fun s25 () (_ BitVec 32) ((_ rotate_left 2) s0)) [GOOD] (define-fun s26 () (_ BitVec 32) ((_ rotate_left 3) s0)) [GOOD] (define-fun s27 () (_ BitVec 32) ((_ rotate_left 4) s0)) [GOOD] (define-fun s28 () (_ BitVec 32) ((_ rotate_left 5) s0)) [GOOD] (define-fun s29 () (_ BitVec 32) ((_ rotate_left 6) s0)) [GOOD] (define-fun s30 () (_ BitVec 32) ((_ rotate_left 7) s0)) [GOOD] (define-fun s31 () (_ BitVec 32) ((_ rotate_left 8) s0)) [GOOD] (define-fun s32 () (_ BitVec 32) ((_ rotate_left 9) s0)) [GOOD] (define-fun s33 () (_ BitVec 32) ((_ rotate_left 10) s0)) [GOOD] (define-fun s34 () (_ BitVec 32) ((_ rotate_left 11) s0)) [GOOD] (define-fun s35 () (_ BitVec 32) ((_ rotate_left 12) s0)) [GOOD] (define-fun s36 () (_ BitVec 32) ((_ rotate_left 13) s0)) [GOOD] (define-fun s37 () (_ BitVec 32) ((_ rotate_left 14) s0)) [GOOD] (define-fun s38 () (_ BitVec 32) ((_ rotate_left 15) s0)) [GOOD] (define-fun s39 () (_ BitVec 32) ((_ rotate_left 16) s0)) [GOOD] (define-fun s40 () (_ BitVec 32) ((_ rotate_left 17) s0)) [GOOD] (define-fun s41 () (_ BitVec 32) ((_ rotate_left 18) s0)) [GOOD] (define-fun s42 () (_ BitVec 32) ((_ rotate_left 19) s0)) [GOOD] (define-fun s43 () (_ BitVec 32) ((_ rotate_left 20) s0)) [GOOD] (define-fun s44 () (_ BitVec 32) ((_ rotate_left 21) s0)) [GOOD] (define-fun s45 () (_ BitVec 32) ((_ rotate_left 22) s0)) [GOOD] (define-fun s46 () (_ BitVec 32) ((_ rotate_left 23) s0)) [GOOD] (define-fun s47 () (_ BitVec 32) ((_ rotate_left 24) s0)) [GOOD] (define-fun s48 () (_ BitVec 32) ((_ rotate_left 25) s0)) [GOOD] (define-fun s49 () (_ BitVec 32) ((_ rotate_left 26) s0)) [GOOD] (define-fun s50 () (_ BitVec 32) ((_ rotate_left 27) s0)) [GOOD] (define-fun s51 () (_ BitVec 32) ((_ rotate_left 28) s0)) [GOOD] (define-fun s52 () (_ BitVec 32) ((_ rotate_left 29) s0)) [GOOD] (define-fun s53 () (_ BitVec 32) ((_ rotate_left 30) s0)) [GOOD] (define-fun s54 () (_ BitVec 32) ((_ rotate_left 31) s0)) [GOOD] (define-fun s56 () (_ BitVec 32) (ite (bvule #x20 s3) s55 (table0 s3))) [GOOD] (define-fun s57 () Bool (= s24 s56)) [GOOD] (assert (= (table0 #x00) s0)) [GOOD] (assert (= (table0 #x01) s15)) [GOOD] (assert (= (table0 #x02) s25)) [GOOD] (assert (= (table0 #x03) s26)) [GOOD] (assert (= (table0 #x04) s27)) [GOOD] (assert (= (table0 #x05) s28)) [GOOD] (assert (= (table0 #x06) s29)) [GOOD] (assert (= (table0 #x07) s30)) [GOOD] (assert (= (table0 #x08) s31)) [GOOD] (assert (= (table0 #x09) s32)) [GOOD] (assert (= (table0 #x0a) s33)) [GOOD] (assert (= (table0 #x0b) s34)) [GOOD] (assert (= (table0 #x0c) s35)) [GOOD] (assert (= (table0 #x0d) s36)) [GOOD] (assert (= (table0 #x0e) s37)) [GOOD] (assert (= (table0 #x0f) s38)) [GOOD] (assert (= (table0 #x10) s39)) [GOOD] (assert (= (table0 #x11) s40)) [GOOD] (assert (= (table0 #x12) s41)) [GOOD] (assert (= (table0 #x13) s42)) [GOOD] (assert (= (table0 #x14) s43)) [GOOD] (assert (= (table0 #x15) s44)) [GOOD] (assert (= (table0 #x16) s45)) [GOOD] (assert (= (table0 #x17) s46)) [GOOD] (assert (= (table0 #x18) s47)) [GOOD] (assert (= (table0 #x19) s48)) [GOOD] (assert (= (table0 #x1a) s49)) [GOOD] (assert (= (table0 #x1b) s50)) [GOOD] (assert (= (table0 #x1c) s51)) [GOOD] (assert (= (table0 #x1d) s52)) [GOOD] (assert (= (table0 #x1e) s53)) [GOOD] (assert (= (table0 #x1f) s54)) [GOOD] (assert (not s57)) [SEND] (check-sat) [RECV] unsat *** Solver : CVC4 *** Exit code: ExitSuccess *** Std-out : FINAL: Q.E.D. DONE!