(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)))