1** Calling: cvc4 --lang smt --incremental --interactive --no-interactive-prompt --model-witness-value 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 :diagnostic-output-channel "stdout") 6[GOOD] (set-option :produce-models true) 7[GOOD] (set-logic QF_UFBV) 8[GOOD] ; --- uninterpreted sorts --- 9[GOOD] ; --- tuples --- 10[GOOD] ; --- sums --- 11[GOOD] ; --- literal constants --- 12[GOOD] (define-fun s2 () (_ BitVec 8) #x40) 13[GOOD] (define-fun s5 () (_ BitVec 1) #b0) 14[GOOD] (define-fun s91 () (_ BitVec 64) #x0000000000000000) 15[GOOD] ; --- skolem constants --- 16[GOOD] (declare-fun s0 () (_ BitVec 64)) 17[GOOD] (declare-fun s1 () (_ BitVec 8)) 18[GOOD] ; --- constant tables --- 19[GOOD] ; --- skolemized tables --- 20[GOOD] (declare-fun table0 ((_ BitVec 8)) (_ BitVec 64)) 21[GOOD] ; --- arrays --- 22[GOOD] ; --- uninterpreted constants --- 23[GOOD] ; --- user given axioms --- 24[GOOD] ; --- formula --- 25[GOOD] (define-fun s3 () (_ BitVec 8) (bvurem s1 s2)) 26[GOOD] (define-fun s4 () (_ BitVec 1) ((_ extract 5 5) s3)) 27[GOOD] (define-fun s6 () Bool (distinct s4 s5)) 28[GOOD] (define-fun s7 () (_ BitVec 1) ((_ extract 4 4) s3)) 29[GOOD] (define-fun s8 () Bool (distinct s5 s7)) 30[GOOD] (define-fun s9 () (_ BitVec 1) ((_ extract 3 3) s3)) 31[GOOD] (define-fun s10 () Bool (distinct s5 s9)) 32[GOOD] (define-fun s11 () (_ BitVec 1) ((_ extract 2 2) s3)) 33[GOOD] (define-fun s12 () Bool (distinct s5 s11)) 34[GOOD] (define-fun s13 () (_ BitVec 1) ((_ extract 1 1) s3)) 35[GOOD] (define-fun s14 () Bool (distinct s5 s13)) 36[GOOD] (define-fun s15 () (_ BitVec 1) ((_ extract 0 0) s3)) 37[GOOD] (define-fun s16 () Bool (distinct s5 s15)) 38[GOOD] (define-fun s17 () (_ BitVec 64) ((_ rotate_right 1) s0)) 39[GOOD] (define-fun s18 () (_ BitVec 64) (ite s16 s17 s0)) 40[GOOD] (define-fun s19 () (_ BitVec 64) ((_ rotate_right 2) s18)) 41[GOOD] (define-fun s20 () (_ BitVec 64) (ite s14 s19 s18)) 42[GOOD] (define-fun s21 () (_ BitVec 64) ((_ rotate_right 4) s20)) 43[GOOD] (define-fun s22 () (_ BitVec 64) (ite s12 s21 s20)) 44[GOOD] (define-fun s23 () (_ BitVec 64) ((_ rotate_right 8) s22)) 45[GOOD] (define-fun s24 () (_ BitVec 64) (ite s10 s23 s22)) 46[GOOD] (define-fun s25 () (_ BitVec 64) ((_ rotate_right 16) s24)) 47[GOOD] (define-fun s26 () (_ BitVec 64) (ite s8 s25 s24)) 48[GOOD] (define-fun s27 () (_ BitVec 64) ((_ rotate_right 32) s26)) 49[GOOD] (define-fun s28 () (_ BitVec 64) (ite s6 s27 s26)) 50[GOOD] (define-fun s29 () (_ BitVec 64) ((_ rotate_right 2) s0)) 51[GOOD] (define-fun s30 () (_ BitVec 64) ((_ rotate_right 3) s0)) 52[GOOD] (define-fun s31 () (_ BitVec 64) ((_ rotate_right 4) s0)) 53[GOOD] (define-fun s32 () (_ BitVec 64) ((_ rotate_right 5) s0)) 54[GOOD] (define-fun s33 () (_ BitVec 64) ((_ rotate_right 6) s0)) 55[GOOD] (define-fun s34 () (_ BitVec 64) ((_ rotate_right 7) s0)) 56[GOOD] (define-fun s35 () (_ BitVec 64) ((_ rotate_right 8) s0)) 57[GOOD] (define-fun s36 () (_ BitVec 64) ((_ rotate_right 9) s0)) 58[GOOD] (define-fun s37 () (_ BitVec 64) ((_ rotate_right 10) s0)) 59[GOOD] (define-fun s38 () (_ BitVec 64) ((_ rotate_right 11) s0)) 60[GOOD] (define-fun s39 () (_ BitVec 64) ((_ rotate_right 12) s0)) 61[GOOD] (define-fun s40 () (_ BitVec 64) ((_ rotate_right 13) s0)) 62[GOOD] (define-fun s41 () (_ BitVec 64) ((_ rotate_right 14) s0)) 63[GOOD] (define-fun s42 () (_ BitVec 64) ((_ rotate_right 15) s0)) 64[GOOD] (define-fun s43 () (_ BitVec 64) ((_ rotate_right 16) s0)) 65[GOOD] (define-fun s44 () (_ BitVec 64) ((_ rotate_right 17) s0)) 66[GOOD] (define-fun s45 () (_ BitVec 64) ((_ rotate_right 18) s0)) 67[GOOD] (define-fun s46 () (_ BitVec 64) ((_ rotate_right 19) s0)) 68[GOOD] (define-fun s47 () (_ BitVec 64) ((_ rotate_right 20) s0)) 69[GOOD] (define-fun s48 () (_ BitVec 64) ((_ rotate_right 21) s0)) 70[GOOD] (define-fun s49 () (_ BitVec 64) ((_ rotate_right 22) s0)) 71[GOOD] (define-fun s50 () (_ BitVec 64) ((_ rotate_right 23) s0)) 72[GOOD] (define-fun s51 () (_ BitVec 64) ((_ rotate_right 24) s0)) 73[GOOD] (define-fun s52 () (_ BitVec 64) ((_ rotate_right 25) s0)) 74[GOOD] (define-fun s53 () (_ BitVec 64) ((_ rotate_right 26) s0)) 75[GOOD] (define-fun s54 () (_ BitVec 64) ((_ rotate_right 27) s0)) 76[GOOD] (define-fun s55 () (_ BitVec 64) ((_ rotate_right 28) s0)) 77[GOOD] (define-fun s56 () (_ BitVec 64) ((_ rotate_right 29) s0)) 78[GOOD] (define-fun s57 () (_ BitVec 64) ((_ rotate_right 30) s0)) 79[GOOD] (define-fun s58 () (_ BitVec 64) ((_ rotate_right 31) s0)) 80[GOOD] (define-fun s59 () (_ BitVec 64) ((_ rotate_right 32) s0)) 81[GOOD] (define-fun s60 () (_ BitVec 64) ((_ rotate_right 33) s0)) 82[GOOD] (define-fun s61 () (_ BitVec 64) ((_ rotate_right 34) s0)) 83[GOOD] (define-fun s62 () (_ BitVec 64) ((_ rotate_right 35) s0)) 84[GOOD] (define-fun s63 () (_ BitVec 64) ((_ rotate_right 36) s0)) 85[GOOD] (define-fun s64 () (_ BitVec 64) ((_ rotate_right 37) s0)) 86[GOOD] (define-fun s65 () (_ BitVec 64) ((_ rotate_right 38) s0)) 87[GOOD] (define-fun s66 () (_ BitVec 64) ((_ rotate_right 39) s0)) 88[GOOD] (define-fun s67 () (_ BitVec 64) ((_ rotate_right 40) s0)) 89[GOOD] (define-fun s68 () (_ BitVec 64) ((_ rotate_right 41) s0)) 90[GOOD] (define-fun s69 () (_ BitVec 64) ((_ rotate_right 42) s0)) 91[GOOD] (define-fun s70 () (_ BitVec 64) ((_ rotate_right 43) s0)) 92[GOOD] (define-fun s71 () (_ BitVec 64) ((_ rotate_right 44) s0)) 93[GOOD] (define-fun s72 () (_ BitVec 64) ((_ rotate_right 45) s0)) 94[GOOD] (define-fun s73 () (_ BitVec 64) ((_ rotate_right 46) s0)) 95[GOOD] (define-fun s74 () (_ BitVec 64) ((_ rotate_right 47) s0)) 96[GOOD] (define-fun s75 () (_ BitVec 64) ((_ rotate_right 48) s0)) 97[GOOD] (define-fun s76 () (_ BitVec 64) ((_ rotate_right 49) s0)) 98[GOOD] (define-fun s77 () (_ BitVec 64) ((_ rotate_right 50) s0)) 99[GOOD] (define-fun s78 () (_ BitVec 64) ((_ rotate_right 51) s0)) 100[GOOD] (define-fun s79 () (_ BitVec 64) ((_ rotate_right 52) s0)) 101[GOOD] (define-fun s80 () (_ BitVec 64) ((_ rotate_right 53) s0)) 102[GOOD] (define-fun s81 () (_ BitVec 64) ((_ rotate_right 54) s0)) 103[GOOD] (define-fun s82 () (_ BitVec 64) ((_ rotate_right 55) s0)) 104[GOOD] (define-fun s83 () (_ BitVec 64) ((_ rotate_right 56) s0)) 105[GOOD] (define-fun s84 () (_ BitVec 64) ((_ rotate_right 57) s0)) 106[GOOD] (define-fun s85 () (_ BitVec 64) ((_ rotate_right 58) s0)) 107[GOOD] (define-fun s86 () (_ BitVec 64) ((_ rotate_right 59) s0)) 108[GOOD] (define-fun s87 () (_ BitVec 64) ((_ rotate_right 60) s0)) 109[GOOD] (define-fun s88 () (_ BitVec 64) ((_ rotate_right 61) s0)) 110[GOOD] (define-fun s89 () (_ BitVec 64) ((_ rotate_right 62) s0)) 111[GOOD] (define-fun s90 () (_ BitVec 64) ((_ rotate_right 63) s0)) 112[GOOD] (define-fun s92 () (_ BitVec 64) (ite (bvule #x40 s3) s91 (table0 s3))) 113[GOOD] (define-fun s93 () Bool (= s28 s92)) 114[GOOD] (assert (= (table0 #x00) s0)) 115[GOOD] (assert (= (table0 #x01) s17)) 116[GOOD] (assert (= (table0 #x02) s29)) 117[GOOD] (assert (= (table0 #x03) s30)) 118[GOOD] (assert (= (table0 #x04) s31)) 119[GOOD] (assert (= (table0 #x05) s32)) 120[GOOD] (assert (= (table0 #x06) s33)) 121[GOOD] (assert (= (table0 #x07) s34)) 122[GOOD] (assert (= (table0 #x08) s35)) 123[GOOD] (assert (= (table0 #x09) s36)) 124[GOOD] (assert (= (table0 #x0a) s37)) 125[GOOD] (assert (= (table0 #x0b) s38)) 126[GOOD] (assert (= (table0 #x0c) s39)) 127[GOOD] (assert (= (table0 #x0d) s40)) 128[GOOD] (assert (= (table0 #x0e) s41)) 129[GOOD] (assert (= (table0 #x0f) s42)) 130[GOOD] (assert (= (table0 #x10) s43)) 131[GOOD] (assert (= (table0 #x11) s44)) 132[GOOD] (assert (= (table0 #x12) s45)) 133[GOOD] (assert (= (table0 #x13) s46)) 134[GOOD] (assert (= (table0 #x14) s47)) 135[GOOD] (assert (= (table0 #x15) s48)) 136[GOOD] (assert (= (table0 #x16) s49)) 137[GOOD] (assert (= (table0 #x17) s50)) 138[GOOD] (assert (= (table0 #x18) s51)) 139[GOOD] (assert (= (table0 #x19) s52)) 140[GOOD] (assert (= (table0 #x1a) s53)) 141[GOOD] (assert (= (table0 #x1b) s54)) 142[GOOD] (assert (= (table0 #x1c) s55)) 143[GOOD] (assert (= (table0 #x1d) s56)) 144[GOOD] (assert (= (table0 #x1e) s57)) 145[GOOD] (assert (= (table0 #x1f) s58)) 146[GOOD] (assert (= (table0 #x20) s59)) 147[GOOD] (assert (= (table0 #x21) s60)) 148[GOOD] (assert (= (table0 #x22) s61)) 149[GOOD] (assert (= (table0 #x23) s62)) 150[GOOD] (assert (= (table0 #x24) s63)) 151[GOOD] (assert (= (table0 #x25) s64)) 152[GOOD] (assert (= (table0 #x26) s65)) 153[GOOD] (assert (= (table0 #x27) s66)) 154[GOOD] (assert (= (table0 #x28) s67)) 155[GOOD] (assert (= (table0 #x29) s68)) 156[GOOD] (assert (= (table0 #x2a) s69)) 157[GOOD] (assert (= (table0 #x2b) s70)) 158[GOOD] (assert (= (table0 #x2c) s71)) 159[GOOD] (assert (= (table0 #x2d) s72)) 160[GOOD] (assert (= (table0 #x2e) s73)) 161[GOOD] (assert (= (table0 #x2f) s74)) 162[GOOD] (assert (= (table0 #x30) s75)) 163[GOOD] (assert (= (table0 #x31) s76)) 164[GOOD] (assert (= (table0 #x32) s77)) 165[GOOD] (assert (= (table0 #x33) s78)) 166[GOOD] (assert (= (table0 #x34) s79)) 167[GOOD] (assert (= (table0 #x35) s80)) 168[GOOD] (assert (= (table0 #x36) s81)) 169[GOOD] (assert (= (table0 #x37) s82)) 170[GOOD] (assert (= (table0 #x38) s83)) 171[GOOD] (assert (= (table0 #x39) s84)) 172[GOOD] (assert (= (table0 #x3a) s85)) 173[GOOD] (assert (= (table0 #x3b) s86)) 174[GOOD] (assert (= (table0 #x3c) s87)) 175[GOOD] (assert (= (table0 #x3d) s88)) 176[GOOD] (assert (= (table0 #x3e) s89)) 177[GOOD] (assert (= (table0 #x3f) s90)) 178[GOOD] (assert (not s93)) 179[SEND] (check-sat) 180[RECV] unsat 181*** Solver : CVC4 182*** Exit code: ExitSuccess 183*** Std-out : 184 185FINAL: 186Q.E.D. 187DONE! 188