Untitled

(set-option :auto-config false)

(set-option :smt.mbqi false)

;(set-option :smt.mbqi.max_iterations 15)

 

;; pow256 and pow255

(define-fun pow256 () Int

  115792089237316195423570985008687907853269984665640564039457584007913129639936)

(define-fun pow255 () Int

  57896044618658097711785492504343953926634992332820282019728792003956564819968)

;; weird declaration trick (doesn't seem to be needed currently)

;; (declare-fun pow256 () Int)

;; (assert (>= pow256 115792089237316195423570985008687907853269984665640564039457584007913129639936))

;; (assert (<= pow256 115792089237316195423570985008687907853269984665640564039457584007913129639936))

 

;; signed word arithmetic definitions:

;; integer to word:

(define-fun unsigned ((x Int)) Int

  (if (>= x 0)

      x

    (+ x pow256)))

 

;; word to integer

(define-fun signed ((x Int)) Int

  (if (< x pow255)

      x

    (- x pow256)))

 

;; signed_abs

(define-fun signed_abs ((x Int)) Int

  (if (< x pow255)

      x

    (- pow256 x)))

 

;; signed_sgn

(define-fun signed_sgn ((x Int)) Int

  (if (< x pow255)

      1

    -1))

 

;; smt_rpow

(declare-fun smt_rpow (Int Int Int Int) Int)

(assert (forall ((z Int) (x Int) (y Int) (b Int)) (! (=> (= y 1) (= (smt_rpow z x y b) (div (+ (* z x) (div b 2)) b))) :pattern ((smt_rpow z x y b)))))

 

(assert (forall ((z1 Int) (z2 Int) (x1 Int) (y1 Int) (x2 Int) (y2 Int) (b1 Int) (b2 Int))

  (!

    (=> (and (<= z1 z2) (<= x1 x2) (<= y1 y2) (<= b1 b2))

      (<= (smt_rpow z1 x1 y1 b1) (smt_rpow z2 x2 y2 b2))

    )

    :pattern ((smt_rpow z1 x1 y1 b1) (smt_rpow z2 x2 y2 b2))

  )

))

 

(assert (forall ((z Int) (x Int) (y Int) (b Int)) (! (=> (>= y 1) (>= (* (smt_rpow z x y b) b) (* z x))) :pattern ((smt_rpow z x y b)))))

(assert (forall ((z Int) (x Int) (y Int) (b Int)) (! (=> (>= y 2) (>= (* (smt_rpow z x y b) b) (* x x))) :pattern ((smt_rpow z x y b)))))

 

(assert (forall ((z Int) (x Int) (y Int) (b Int)) (! (=> (>= y 1) (>= (* (smt_rpow z x y b) b) (+ (* z x) (div b 2)))) :pattern ((smt_rpow z x y b)))))

(assert (forall ((z Int) (x Int) (y Int) (b Int)) (! (=> (>= y 2) (>= (* (smt_rpow z x y b) b) (+ (* x x) (div b 2)))) :pattern ((smt_rpow z x y b)))))

;

; end of prelude

;

(declare-sort IntList)

(declare-sort Bytes)

(declare-sort WordStack)

(declare-fun sizeWordStackAux (WordStack Int) Int)

(declare-fun word_mod (Int Int) Int)

(declare-fun word_plus (Int Int) Int)

(declare-fun word_sub (Int Int) Int)

(declare-fun smt_keccakIntList (IntList) Int)

(declare-fun lengthBytesAux (Bytes Int) Int)

(declare-fun sizeWordStack (WordStack) Int)

(declare-fun smt_keccak (WordStack) Int)

(declare-fun asByteStack (Int WordStack) WordStack)

(declare-fun word_div (Int Int) Int)

(declare-fun chop (Int) Int)

(declare-fun lengthBytes (Bytes) Int)

(declare-fun smt_nthbyteof (Int Int Int) Int)

(declare-fun word_times (Int Int) Int)

(declare-fun asWord (WordStack) Int)

(declare-fun expFunc (Int Int) Int)

(assert (forall ((|_125_R_I| Int)) (= (chop |_125_R_I|) (mod |_125_R_I| pow256))))

(assert (forall ((|_393_R__533| Int)(|_392_R__532| WordStack)) (= (>= (sizeWordStackAux |_392_R__532| |_393_R__533|) 0) true)))

(declare-fun |_1961_ABI_wad| () Int)

(declare-fun |_2007_Vat_balance| () Int)

(declare-fun |_1952_ORIGIN_ID| () Int)

(declare-fun |_1962_ACCT_ID| () Int)

(declare-fun |_1954_Dai_dst| () Int)

(declare-fun |_1965_Vat| () Int)

(declare-fun |_1964_Can| () Int)

(declare-fun |_1953_ACCT_ID_balance| () Int)

(declare-fun |_2008_VCallDepth| () Int)

(declare-fun |_1967_VGas| () Int)

(declare-fun |_1966_TIME| () Int)

(declare-fun |_1955_Dai_src| () Int)

(declare-fun |_1959_ABI_dst| () Int)

(declare-fun |_2012_CALLER_ID| () Int)

(declare-fun |_279753_| () Bool)

(declare-fun |_279755_| () Bool)

(declare-fun |_279752_| () Bool)

(declare-fun |_279756_| () Bool)

(declare-fun |_279754_| () Bool)

(declare-fun |_1869_Dai_src| () Int)

(assert (and (and

 (= (<= 0 |_1961_ABI_wad|) true)

 (= _279752_ false)

 (= (<= |_2012_CALLER_ID| 1461501637330902918203684832716283019655932542975) true)

 (= (<= (+ |_1954_Dai_dst| (* 1000000000000000000000000000 |_1961_ABI_wad|)) 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)

 (= (<= 0 |_1965_Vat|) true)

 (= (<= 0 |_1952_ORIGIN_ID|) true)

 (= (<= 9 |_1962_ACCT_ID|) true)

 (= (<= |_1966_TIME| 281474976710655) true)

 (= (= |_1961_ABI_wad| 0) false)

 (= (<= 0 |_2012_CALLER_ID|) true)

 (= (<= (- |_1955_Dai_src| (* 1000000000000000000000000000 |_1961_ABI_wad|)) 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)

 (= (<= |_2008_VCallDepth| 1024) true)

 (= (<= |_1954_Dai_dst| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)

 (= (<= 0 |_2007_Vat_balance|) true)

 (= (<= |_1961_ABI_wad| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)

 (= (<= |_1959_ABI_dst| 1461501637330902918203684832716283019655932542975) true)

 (= (<= 0 |_1955_Dai_src|) true)

 (= (<= 0 |_1964_Can|) true)

 (= _279753_ false)

 (= (= |_1962_ACCT_ID| |_1965_Vat|) false)

 (= (<= -57896044618658097711785492504343953926634992332820282019728792003956564819968 (* 1000000000000000000000000000 |_1961_ABI_wad|)) true)

 (= (<= 0 |_1959_ABI_dst|) true)

 (= (<= 0 (+ |_1954_Dai_dst| (* 1000000000000000000000000000 |_1961_ABI_wad|))) true)

 (= _279754_ false)

 (= (<= |_1953_ACCT_ID_balance| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)

 (= (<= 9 |_1965_Vat|) true)

 (= (>= |_1967_VGas| 3000000) true)

 (= _279755_ false)

 (= (<= 0 |_1954_Dai_dst|) true)

 (= (< |_2008_VCallDepth| 1024) true)

 (= (<= (* 1000000000000000000000000000 |_1961_ABI_wad|) 57896044618658097711785492504343953926634992332820282019728792003956564819967) true)

 (= (<= 0 (- |_1955_Dai_src| (* 1000000000000000000000000000 |_1961_ABI_wad|))) true)

 (= (<= |_1952_ORIGIN_ID| 1461501637330902918203684832716283019655932542975) true)

 (= (<= |_1965_Vat| 1461501637330902918203684832716283019655932542975) true)

 (= (<= 0 |_1962_ACCT_ID|) true)

 (= (<= 0 |_1966_TIME|) true)

 (= _279756_ false)

 (= (<= 0 |_1953_ACCT_ID_balance|) true)

 (= (<= |_1964_Can| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)

 (= (<= |_1962_ACCT_ID| 1461501637330902918203684832716283019655932542975) true)

 (= (<= |_1955_Dai_src| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)

 (= (<= |_2007_Vat_b1111728884 alance| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)

 (= (= |_2012_CALLER_ID| |_1959_ABI_dst|) false))

(not (and

 (= (and (not (= (- |_1869_Dai_src| (* 1000000000000000000000000000 |_1961_ABI_wad|)) 0)) (= |_1869_Dai_src| 0)) false)))))(check-sat-using (or-else (using-params smt :random-seed 3 :timeout 1000) (using-params smt :random-seed 2 :timeout 2000) (using-params smt :random-seed 1)))