explore

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; SBV: Starting at 2020-06-02 17:05:41.766748 CEST
;;;
;;;           Solver    : Z3
;;;           Executable: /nix/store/ac646i28c44y2s3p5wy0zlhrlcx0x039-z3-4.8.5/bin/z3
;;;           Options   : -nw -in -smt2
;;;
;;; This file is an auto-generated loadable SMT-Lib file.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; [17:05:41.767] [Timeout: 5s] Sending:
(set-option :print-success true)
; [17:05:41.770] Received: success
; [17:05:41.770] Sending:
(set-option :global-declarations true)
; [17:05:41.770] Received: success
; [17:05:41.770] Sending:
(set-option :smtlib2_compliant true)
; [17:05:41.770] Received: success
; [17:05:41.771] Sending:
(set-option :diagnostic-output-channel "stdout")
; [17:05:41.771] Received: success
; [17:05:41.771] Sending:
(set-option :produce-models true)
; [17:05:41.771] Received: success
; [17:05:41.771] Sending:
(set-logic ALL) ; external query, using all logics.
; [17:05:41.771] Received: success
; [17:05:41.771] Sending:
(declare-fun s0 () (_ BitVec 256))
; [17:05:41.779] Received: success
; [17:05:41.779] Sending:
(declare-fun s1 () (_ BitVec 256))
; [17:05:41.779] Received: success
; [17:05:41.779] Sending:
(declare-fun s2 () (_ BitVec 256))
; [17:05:41.779] Received: success
; [17:05:41.780] Sending:
(declare-fun s3 () (_ BitVec 256))
; [17:05:41.780] Received: success
; [17:05:41.780] Sending:
(declare-fun s4 () (_ BitVec 256))
; [17:05:41.780] Received: success
; [17:05:41.780] Sending:
(declare-fun s5 () (_ BitVec 256))
; [17:05:41.780] Received: success
; [17:05:41.781] Sending:
(declare-fun s6 () (_ BitVec 256))
; [17:05:41.781] Received: success
; [17:05:41.781] Sending:
(declare-fun s7 () (_ BitVec 256))
; [17:05:41.781] Received: success
; [17:05:41.781] Sending:
(declare-fun s8 () (_ BitVec 32))
; [17:05:41.781] Received: success
; [17:05:41.781] Sending:
(declare-fun array_0 () (Array (_ BitVec 256) (_ BitVec 256)))
; [17:05:41.781] Received: success
; [17:05:41.782] Sending:
(define-fun s9 () (_ BitVec 32) #x00000400)
; [17:05:41.782] Received: success
; [17:05:41.782] Sending:
(define-fun s10 () Bool (bvule s8 s9))
; [17:05:41.783] Received: success
; [17:05:41.783] Sending:
(assert s10)
; [17:05:41.783] Received: success
; [17:05:41.783] Sending:
(define-fun s11 () (_ BitVec 224) #x00000000000000000000000000000000000000000000000000000000)
; [17:05:41.783] Received: success
; [17:05:41.783] Sending:
(define-fun s13 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000004)
; [17:05:41.783] Received: success
; [17:05:41.783] Sending:
(define-fun s15 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000001)
; [17:05:41.784] Received: success
; [17:05:41.784] Sending:
(define-fun s16 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000)
; [17:05:41.784] Received: success
; [17:05:41.784] Sending:
(define-fun s12 () (_ BitVec 256) (concat s11 s8))
; [17:05:41.784] Received: success
; [17:05:41.784] Sending:
(define-fun s14 () Bool (bvult s12 s13))
; [17:05:41.784] Received: success
; [17:05:41.784] Sending:
(define-fun s17 () (_ BitVec 256) (ite s14 s15 s16))
; [17:05:41.785] Received: success
; [17:05:41.785] Sending:
(define-fun s18 () Bool (= s16 s17))
; [17:05:41.785] Received: success
; [17:05:41.785] Sending:
(define-fun s19 () Bool (not s18))
; [17:05:41.785] Received: success
; [17:05:41.785] Sending:
(assert s19)
; [17:05:41.785] Received: success
; [17:05:41.785] Sending:
(check-sat)
; [17:05:41.797] Received: sat
; [17:05:41.797] Sending:
(reset-assertions)
; [17:05:41.803] Received: success
; [17:05:41.803] Sending:
(assert s10)
; [17:05:41.805] Received: success
; [17:05:41.806] Sending:
(assert s18)
; [17:05:41.806] Received: success
; [17:05:41.806] Sending:
(check-sat)
; [17:05:41.818] Received: sat
; [17:05:41.818] Sending:
(reset-assertions)
; [17:05:41.823] Received: success
; [17:05:41.823] Sending:
(define-fun s20 () Bool (and s10 s18))
; [17:05:41.823] Received: success
; [17:05:41.823] Sending:
(assert s20)
; [17:05:41.825] Received: success
; [17:05:41.825] Sending:
(define-fun s21 () (_ BitVec 256) #x00000000000000000000000000000000000000000000000000000000b3de648b)
; [17:05:41.826] Received: success
; [17:05:41.826] Sending:
(define-fun s85 () (_ BitVec 256) #x00000000000000000000000000000000000000000000000000000000000000e0)
; [17:05:41.826] Received: success
; [17:05:41.827] Sending:
(define-fun s22 () (_ BitVec 8) ((_ extract 255 248) s0))
; [17:05:41.827] Received: success
; [17:05:41.827] Sending:
(define-fun s23 () (_ BitVec 8) ((_ extract 247 240) s0))
; [17:05:41.827] Received: success
; [17:05:41.827] Sending:
(define-fun s24 () (_ BitVec 16) (concat s22 s23))
; [17:05:41.828] Received: success
; [17:05:41.828] Sending:
(define-fun s25 () (_ BitVec 8) ((_ extract 239 232) s0))
; [17:05:41.828] Received: success
; [17:05:41.828] Sending:
(define-fun s26 () (_ BitVec 8) ((_ extract 231 224) s0))
; [17:05:41.828] Received: success
; [17:05:41.828] Sending:
(define-fun s27 () (_ BitVec 16) (concat s25 s26))
; [17:05:41.828] Received: success
; [17:05:41.829] Sending:
(define-fun s28 () (_ BitVec 32) (concat s24 s27))
; [17:05:41.829] Received: success
; [17:05:41.829] Sending:
(define-fun s29 () (_ BitVec 8) ((_ extract 223 216) s0))
; [17:05:41.829] Received: success
; [17:05:41.829] Sending:
(define-fun s30 () (_ BitVec 8) ((_ extract 215 208) s0))
; [17:05:41.829] Received: success
; [17:05:41.829] Sending:
(define-fun s31 () (_ BitVec 16) (concat s29 s30))
; [17:05:41.829] Received: success
; [17:05:41.830] Sending:
(define-fun s32 () (_ BitVec 8) ((_ extract 207 200) s0))
; [17:05:41.830] Received: success
; [17:05:41.830] Sending:
(define-fun s33 () (_ BitVec 8) ((_ extract 199 192) s0))
; [17:05:41.830] Received: success
; [17:05:41.830] Sending:
(define-fun s34 () (_ BitVec 16) (concat s32 s33))
; [17:05:41.830] Received: success
; [17:05:41.830] Sending:
(define-fun s35 () (_ BitVec 32) (concat s31 s34))
; [17:05:41.830] Received: success
; [17:05:41.830] Sending:
(define-fun s36 () (_ BitVec 64) (concat s28 s35))
; [17:05:41.831] Received: success
; [17:05:41.831] Sending:
(define-fun s37 () (_ BitVec 8) ((_ extract 191 184) s0))
; [17:05:41.831] Received: success
; [17:05:41.831] Sending:
(define-fun s38 () (_ BitVec 8) ((_ extract 183 176) s0))
; [17:05:41.831] Received: success
; [17:05:41.831] Sending:
(define-fun s39 () (_ BitVec 16) (concat s37 s38))
; [17:05:41.831] Received: success
; [17:05:41.831] Sending:
(define-fun s40 () (_ BitVec 8) ((_ extract 175 168) s0))
; [17:05:41.831] Received: success
; [17:05:41.832] Sending:
(define-fun s41 () (_ BitVec 8) ((_ extract 167 160) s0))
; [17:05:41.832] Received: success
; [17:05:41.832] Sending:
(define-fun s42 () (_ BitVec 16) (concat s40 s41))
; [17:05:41.832] Received: success
; [17:05:41.833] Sending:
(define-fun s43 () (_ BitVec 32) (concat s39 s42))
; [17:05:41.833] Received: success
; [17:05:41.833] Sending:
(define-fun s44 () (_ BitVec 8) ((_ extract 159 152) s0))
; [17:05:41.833] Received: success
; [17:05:41.833] Sending:
(define-fun s45 () (_ BitVec 8) ((_ extract 151 144) s0))
; [17:05:41.833] Received: success
; [17:05:41.833] Sending:
(define-fun s46 () (_ BitVec 16) (concat s44 s45))
; [17:05:41.833] Received: success
; [17:05:41.833] Sending:
(define-fun s47 () (_ BitVec 8) ((_ extract 143 136) s0))
; [17:05:41.834] Received: success
; [17:05:41.834] Sending:
(define-fun s48 () (_ BitVec 8) ((_ extract 135 128) s0))
; [17:05:41.834] Received: success
; [17:05:41.834] Sending:
(define-fun s49 () (_ BitVec 16) (concat s47 s48))
; [17:05:41.834] Received: success
; [17:05:41.834] Sending:
(define-fun s50 () (_ BitVec 32) (concat s46 s49))
; [17:05:41.834] Received: success
; [17:05:41.834] Sending:
(define-fun s51 () (_ BitVec 64) (concat s43 s50))
; [17:05:41.835] Received: success
; [17:05:41.835] Sending:
(define-fun s52 () (_ BitVec 128) (concat s36 s51))
; [17:05:41.835] Received: success
; [17:05:41.835] Sending:
(define-fun s53 () (_ BitVec 8) ((_ extract 127 120) s0))
; [17:05:41.835] Received: success
; [17:05:41.835] Sending:
(define-fun s54 () (_ BitVec 8) ((_ extract 119 112) s0))
; [17:05:41.835] Received: success
; [17:05:41.835] Sending:
(define-fun s55 () (_ BitVec 16) (concat s53 s54))
; [17:05:41.836] Received: success
; [17:05:41.836] Sending:
(define-fun s56 () (_ BitVec 8) ((_ extract 111 104) s0))
; [17:05:41.836] Received: success
; [17:05:41.836] Sending:
(define-fun s57 () (_ BitVec 8) ((_ extract 103 96) s0))
; [17:05:41.836] Received: success
; [17:05:41.836] Sending:
(define-fun s58 () (_ BitVec 16) (concat s56 s57))
; [17:05:41.836] Received: success
; [17:05:41.836] Sending:
(define-fun s59 () (_ BitVec 32) (concat s55 s58))
; [17:05:41.836] Received: success
; [17:05:41.837] Sending:
(define-fun s60 () (_ BitVec 8) ((_ extract 95 88) s0))
; [17:05:41.837] Received: success
; [17:05:41.837] Sending:
(define-fun s61 () (_ BitVec 8) ((_ extract 87 80) s0))
; [17:05:41.837] Received: success
; [17:05:41.837] Sending:
(define-fun s62 () (_ BitVec 16) (concat s60 s61))
; [17:05:41.837] Received: success
; [17:05:41.838] Sending:
(define-fun s63 () (_ BitVec 8) ((_ extract 79 72) s0))
; [17:05:41.838] Received: success
; [17:05:41.838] Sending:
(define-fun s64 () (_ BitVec 8) ((_ extract 71 64) s0))
; [17:05:41.838] Received: success
; [17:05:41.838] Sending:
(define-fun s65 () (_ BitVec 16) (concat s63 s64))
; [17:05:41.838] Received: success
; [17:05:41.838] Sending:
(define-fun s66 () (_ BitVec 32) (concat s62 s65))
; [17:05:41.838] Received: success
; [17:05:41.839] Sending:
(define-fun s67 () (_ BitVec 64) (concat s59 s66))
; [17:05:41.839] Received: success
; [17:05:41.839] Sending:
(define-fun s68 () (_ BitVec 8) ((_ extract 63 56) s0))
; [17:05:41.839] Received: success
; [17:05:41.839] Sending:
(define-fun s69 () (_ BitVec 8) ((_ extract 55 48) s0))
; [17:05:41.839] Received: success
; [17:05:41.839] Sending:
(define-fun s70 () (_ BitVec 16) (concat s68 s69))
; [17:05:41.839] Received: success
; [17:05:41.840] Sending:
(define-fun s71 () (_ BitVec 8) ((_ extract 47 40) s0))
; [17:05:41.840] Received: success
; [17:05:41.840] Sending:
(define-fun s72 () (_ BitVec 8) ((_ extract 39 32) s0))
; [17:05:41.840] Received: success
; [17:05:41.840] Sending:
(define-fun s73 () (_ BitVec 16) (concat s71 s72))
; [17:05:41.840] Received: success
; [17:05:41.840] Sending:
(define-fun s74 () (_ BitVec 32) (concat s70 s73))
; [17:05:41.840] Received: success
; [17:05:41.840] Sending:
(define-fun s75 () (_ BitVec 8) ((_ extract 31 24) s0))
; [17:05:41.841] Received: success
; [17:05:41.841] Sending:
(define-fun s76 () (_ BitVec 8) ((_ extract 23 16) s0))
; [17:05:41.841] Received: success
; [17:05:41.841] Sending:
(define-fun s77 () (_ BitVec 16) (concat s75 s76))
; [17:05:41.841] Received: success
; [17:05:41.841] Sending:
(define-fun s78 () (_ BitVec 8) ((_ extract 15 8) s0))
; [17:05:41.841] Received: success
; [17:05:41.841] Sending:
(define-fun s79 () (_ BitVec 8) ((_ extract 7 0) s0))
; [17:05:41.841] Received: success
; [17:05:41.842] Sending:
(define-fun s80 () (_ BitVec 16) (concat s78 s79))
; [17:05:41.842] Received: success
; [17:05:41.842] Sending:
(define-fun s81 () (_ BitVec 32) (concat s77 s80))
; [17:05:41.842] Received: success
; [17:05:41.842] Sending:
(define-fun s82 () (_ BitVec 64) (concat s74 s81))
; [17:05:41.842] Received: success
; [17:05:41.842] Sending:
(define-fun s83 () (_ BitVec 128) (concat s67 s82))
; [17:05:41.842] Received: success
; [17:05:41.842] Sending:
(define-fun s84 () (_ BitVec 256) (concat s52 s83))
; [17:05:41.843] Received: success
; [17:05:41.843] Sending:
(define-fun s86 () (_ BitVec 256) (bvlshr s84 s85))
; [17:05:41.843] Received: success
; [17:05:41.843] Sending:
(define-fun s87 () Bool (= s21 s86))
; [17:05:41.843] Received: success
; [17:05:41.843] Sending:
(define-fun s88 () (_ BitVec 256) (ite s87 s15 s16))
; [17:05:41.844] Received: success
; [17:05:41.844] Sending:
(define-fun s89 () Bool (= s16 s88))
; [17:05:41.844] Received: success
; [17:05:41.844] Sending:
(define-fun s90 () Bool (not s89))
; [17:05:41.844] Received: success
; [17:05:41.844] Sending:
(assert s90)
; [17:05:41.844] Received: success
; [17:05:41.844] Sending:
(check-sat)
; [17:05:41.854] Received: sat
; [17:05:41.854] Sending:
(reset-assertions)
; [17:05:41.859] Received: success
; [17:05:41.859] Sending:
(assert s20)
; [17:05:41.861] Received: success
; [17:05:41.862] Sending:
(assert s89)
; [17:05:41.862] Received: success
; [17:05:41.862] Sending:
(check-sat)
; [17:05:41.872] Received: sat
; [17:05:41.872] Sending:
(reset-assertions)
; [17:05:41.877] Received: success
; [17:05:41.877] Sending:
(define-fun s91 () Bool (= s15 s88))
; [17:05:41.877] Received: success
; [17:05:41.878] Sending:
(define-fun s92 () Bool (and s18 s91))
; [17:05:41.878] Received: success
; [17:05:41.878] Sending:
(define-fun s93 () Bool (and s10 s92))
; [17:05:41.878] Received: success
; [17:05:41.878] Sending:
(assert s93)
; [17:05:41.880] Received: success
; [17:05:41.880] Sending:
(define-fun s94 () (_ BitVec 256) #xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc)
; [17:05:41.880] Received: success
; [17:05:41.880] Sending:
(define-fun s96 () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000020)
; [17:05:41.880] Received: success
; [17:05:41.880] Sending:
(define-fun s95 () (_ BitVec 256) (bvadd s12 s94))
; [17:05:41.880] Received: success
; [17:05:41.880] Sending:
(define-fun s97 () Bool (bvult s95 s96))
; [17:05:41.881] Received: success
; [17:05:41.881] Sending:
(define-fun s98 () (_ BitVec 256) (ite s97 s15 s16))
; [17:05:41.881] Received: success
; [17:05:41.881] Sending:
(define-fun s99 () Bool (= s16 s98))
; [17:05:41.882] Received: success
; [17:05:41.882] Sending:
(define-fun s100 () (_ BitVec 256) (ite s99 s15 s16))
; [17:05:41.882] Received: success
; [17:05:41.882] Sending:
(define-fun s101 () Bool (= s16 s100))
; [17:05:41.882] Received: success
; [17:05:41.882] Sending:
(define-fun s102 () Bool (not s101))
; [17:05:41.882] Received: success
; [17:05:41.882] Sending:
(assert s102)
; [17:05:41.883] Received: success
; [17:05:41.883] Sending:
(check-sat)
; [17:05:55.714] Received: sat
; [17:05:55.714] Sending:
(reset-assertions)
; [17:05:55.719] Received: success
; [17:05:55.719] Sending:
(assert s93)
; [17:05:55.720] Received: success
; [17:05:55.721] Sending:
(assert s101)
; [17:05:55.721] Received: success
; [17:05:55.721] Sending:
(check-sat)