Jug_drip_fail_contradiction.md

All constraints:

(May ==K 1)                                                                                                                                                                                                 
( Live ==K 1 )                                                                                                                                                                                              
( VCallValue ==K 0 )                                                                                                                                                                                        
( ( ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) <= 0 ) )                                                                                         
( ( minSInt256 <= ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) )                                                                                
( ( ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) <= maxSInt256 ) )                                                                                
( ( minSInt256 <= Art_i ) )                                                                                                                                                                                 
( ( Art_i <= maxSInt256 ) )                                                                                                                                                                                 
( ( 0 < ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) )                                                                                                      
( ( 0 <= ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) )                                                                                                     
( ( minSInt256 <= Rate ) )                                                                                                                                                                                  
( ( Rate <= maxSInt256 ) )                                                                                                                                                                                  
( ( 0 <= ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) ) )                                                                                                                           
( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) <= maxUInt256 ) )                                                                                                                  
( ( Rate ==K 0 ) ==K false )                                                                                                                                                                                
( ( ( Base + Duty ) <= maxUInt256 ) )                                                                                                                                                                       
( ( 0 > ACCT_ID_balance ) ==K false )                                                                                                                                                                       
( ( VCallDepth >= 1024 ) ==K false )                                                                                                                                                                        
( ( Rho <= TIME ) )                                                                                                                                                                                         
( ( 0 <= ACCT_ID ) )                                                                                                                                                                                        
( ( ACCT_ID <= maxUInt160 ) )                                                                                                                                                                               
( ( 0 < ACCT_ID ) )                                                                                                                                                                                         
( ( 9 <= ACCT_ID ) )                                                                                                                                                                                        
( ( 0 <= CALLER_ID ) )                                                                                                                                                                                      
( ( CALLER_ID <= maxUInt160 ) )                                                                                                                                                                             
( ( 0 <= ORIGIN_ID ) )                                                                                                                                                                                      
( ( ORIGIN_ID <= maxUInt160 ) )                                                                                                                                                                             
( ( 0 <= TIME ) )                                                                                                                                                                                           
( ( TIME <= maxUInt256 ) )                                                                                                                                                                                  
( ( 0 <= ACCT_ID_balance ) )                                                                                                                                                                                
( ( ACCT_ID_balance <= maxUInt256 ) )                                                                                                                                                                       
( ( 0 <= ECREC_BAL ) )                                                                                                                                                                                      
( ( ECREC_BAL <= maxUInt256 ) )                                                                                                                                                                             
( ( 0 <= SHA256_BAL ) )                                                                                                                                                                                     
( ( SHA256_BAL <= maxUInt256 ) )                                                                                                                                                                            
( ( 0 <= RIP160_BAL ) )                                                                                                                                                                                     
( ( RIP160_BAL <= maxUInt256 ) )                                                                                                                                                                            
( ( 0 <= ID_BAL ) )                                                                                                                                                                                         
( ( ID_BAL <= maxUInt256 ) )                                                                                                                                                                                
( ( 0 <= MODEXP_BAL ) )                                                                                                                                                                                     
( ( MODEXP_BAL <= maxUInt256 ) )                                                                                                                                                                            
( ( 0 <= ECADD_BAL ) )                                                                                                                                                                                      
( ( ECADD_BAL <= maxUInt256 ) )                                                                                                                                                                             
( ( 0 <= ECMUL_BAL ) )                                                                                                                                                                                      
( ( ECMUL_BAL <= maxUInt256 ) )                                                                                                                                                                             
( ( 0 <= ECPAIRING_BAL ) )                                                                                                                                                                                  
( ( ECPAIRING_BAL <= maxUInt256 ) )                                                                                                                                                                         
( ( VCallDepth <= 1024 ) )                                                                                                                                                                                  
( ( 0 <= ABI_ilk ) )                                                                                                                                                                                        
( ( ABI_ilk <= maxUInt256 ) )                                                                                                                                                                               
( ( 0 <= Vat ) )                                                                                                                                                                                            
( ( Vat <= maxUInt160 ) )                                      
( ( 0 <= Base ) )                                                                                                                                                                                           
( ( Base <= maxUInt256 ) )                                                                                                                                                                                  
( ( 0 <= Vow ) )                                                                                                                                                                                            
( ( Vow <= maxUInt160 ) )                                                                                                                                                                                   
( ( 0 <= Duty ) )                                                                                                                                                                                           
( ( Duty <= maxUInt256 ) )                                                                                                                                                                                  
( ( 0 <= Rho ) )                                                                                                                                                                                            
( ( Rho <= maxUInt48 ) )                                                                                                                                                                                    
( ( 0 <= Rate ) )                                                                                                                                                                                           
( ( Rate <= maxUInt256 ) )                                                                                                                                                                                  
( ( 0 <= Art_i ) )                                                                                                                                                                                          
( ( Art_i <= maxUInt256 ) )                                                                                                                                                                                 
( ( 0 <= Dai ) )                                                                                                                                                                                            
( ( Dai <= maxUInt256 ) )                                                                                                                                                                                   
( ( 0 <= Debt ) )                                                                                                                                                                                           
( ( Debt <= maxUInt256 ) )                                                                                                                                                                                  
( ( 0 <= Ilk_spot ) )                                                                                                                                                                                       
( ( Ilk_spot <= maxUInt256 ) )                                                                                                                                                                              
( ( 0 <= Ilk_line ) )                                                                                                                                                                                       
( ( Ilk_line <= maxUInt256 ) )                                                                                                                                                                              
( ( 0 <= Ilk_dust ) )                                                                                                                                                                                       
( ( Ilk_dust <= maxUInt256 ) )                                                                                                                                                                              
( ( 0 <= Vat_balance ) )                                                                                                                                                                                    
( ( Vat_balance <= maxUInt256 ) )                                                                                                                                                                           
( ( sizeWordStackAux(CD, 0) <= 1250000000 ) )                                                                                                                                                               
( ( 0 < Vat ) )                                                                                                                                                                                             
( ( 9 <= Vat ) )                                                                                                                                                                                            
( ( 0 < Vow ) )                                                                                                                                                                                             
( ( 9 <= Vow ) )                                                                                                                                                                                            
( ( ACCT_ID ==K Vat ) ==K false )                                                                                                                                                                           
( ( num0(( TIME - Rho )) >= 0 ) )                                                                                                                                                                           
( ( num1(( TIME - Rho )) >= 0 ) )                                                                                                                                                                           
( ( 0 <= (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) ) )                                                                                                                                      
( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * #Ray ) < pow256 ) )                                                                                                                       
( ( VGas >= ( 300000000 + (#if ( ( Base + Duty ) ==K 0 ) #then ( 82 + (#if ( ( TIME - Rho ) ==K 0 ) #then 0 #else 10 #fi) ) #else (#if ( ( ( TIME - Rho ) modInt 2 ) ==K 0 ) #then (#if ( ( ( TIME - Rho )  
/ 2 ) ==K 0 ) #then 150 #else ( ( ( num0(( TIME - Rho )) - 1 ) * 172 ) + ( 437 + ( num1(( TIME - Rho )) * 287 ) ) ) #fi) #else (#if ( ( ( TIME - Rho ) / 2 ) ==K 0 ) #then 160 #else ( ( num0(( TIME - Rho  
)) * 172 ) + ( 447 + ( ( num1(( TIME - Rho )) - 1 ) * 287 ) ) ) #fi) #fi) #fi) ) ) )                                                                                                                        
( ( ( VCallDepth < 1024 ) andBool ( ( ( 0 <= ( TIME - Rho ) ) andBool ( ( TIME - Rho ) <= maxUInt256 ) ) andBool ( ( ( 0 <= ( Base + Duty ) ) andBool ( ( Base + Duty ) <= maxUInt256 ) ) andBool ( ( ( 0   
<= ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) ) andBool ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) <= maxUInt256 ) ) andBool ( ( ( 0 <= ( Dai + (     
Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) ) andBool ( ( Dai + ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate 
) / #Ray ) - Rate ) ) ) <= maxUInt256 ) ) andBool ( ( ( 0 <= ( Debt + ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) ) andBool ( ( Debt + ( Art_i 
* ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) <= maxUInt256 ) ) andBool ( ( ( minSInt256 <= Rate ) andBool ( Rate <= maxSInt256 ) ) andBool ( ( (        
minSInt256 <= Art_i ) andBool ( Art_i <= maxSInt256 ) ) andBool ( ( minSInt256 <= ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) andBool ( (      
Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) <= maxSInt256 ) ) ) ) ) ) ) ) ) ) ==K false )                                                          
( ( 0 <= ( Base + Duty ) ) )                                                                                                                                                                                
( ( 0 <= ( TIME - Rho ) ) )                                                                                                                                                                                
( ( ( TIME - Rho ) <= maxUInt256 ) )                                                                                                                                                                        
( ( 0 < ( VGas - ( 5013 + (#if ( ( Base + Duty ) ==K 0 ) #then ( 82 + (#if ( ( TIME - Rho ) ==K 0 ) #then 0 #else 10 #fi) ) #else (#if ( ( ( TIME - Rho ) modInt 2 ) ==K 0 ) #then (#if ( ( ( TIME - Rho )  
/ 2 ) ==K 0 ) #then 150 #else ( ( ( num0(( TIME - Rho )) - 1 ) * 172 ) + ( 437 + ( num1(( TIME - Rho )) * 287 ) ) ) #fi) #else (#if ( ( ( TIME - Rho ) / 2 ) ==K 0 ) #then 160 #else ( ( num0(( TIME - Rho  
)) * 172 ) + ( 447 + ( ( num1(( TIME - Rho )) - 1 ) * 287 ) ) ) #fi) #fi) #fi) ) ) ) )  

Near the bottom, there is the following large constraint (bascially the negation of all the necessary conditions from the pass spec):

( ( ( VCallDepth < 1024 ) andBool ( ( ( 0 <= ( TIME - Rho ) ) andBool ( ( TIME - Rho ) <= maxUInt256 ) ) andBool ( ( ( 0 <= ( Base + Duty ) ) andBool ( ( Base + Duty ) <= maxUInt256 ) ) andBool ( ( ( 0   
<= ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) ) andBool ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) <= maxUInt256 ) ) andBool ( ( ( 0 <= ( Dai + (     
Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) ) andBool ( ( Dai + ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate 
) / #Ray ) - Rate ) ) ) <= maxUInt256 ) ) andBool ( ( ( 0 <= ( Debt + ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) ) andBool ( ( Debt + ( Art_i 
* ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) <= maxUInt256 ) ) andBool ( ( ( minSInt256 <= Rate ) andBool ( Rate <= maxSInt256 ) ) andBool ( ( (        
minSInt256 <= Art_i ) andBool ( Art_i <= maxSInt256 ) ) andBool ( ( minSInt256 <= ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) andBool ( (      
Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) <= maxSInt256 ) ) ) ) ) ) ) ) ) ) ==K false )

I claim this constraint is contradicted by the rest. I will show that under the assumption that the other constraints hold, all individual conditions in this constraint are true, and thus their union via andBool cannot be false.

1. ( VCallDepth < 1024 )

True because ( ( VCallDepth >= 1024 ) ==K false ) is also a constraint.

2. ( ( 0 <= ( TIME - Rho ) ) andBool ( ( TIME - Rho ) <= maxUInt256 ) )

Follows from the following constraints:

• ( ( Rho <= TIME ) )
• ( ( 0 <= Rho ) )
• ( ( 0 <= TIME ) )
• ( ( TIME <= maxUInt256 ) )

3. ( ( 0 <= ( Base + Duty ) ) andBool ( ( Base + Duty ) <= maxUInt256 ) )

Follows from the following constraints:

• ( ( ( Base + Duty ) <= maxUInt256 ) )
• ( ( 0 <= Base ) )
• ( 0 <= Duty ) )

4. ( ( 0 <= ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) ) andBool ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) <= maxUInt256 ) )

Follows from the following constraints:

• ( ( 0 <= ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) ) )
• ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) <= maxUInt256 ) )

5. ( ( 0 <= ( Dai + (Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) ) andBool ( ( Dai + ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) <= maxUInt256 ) )

To show this I will first show that under the constraints given, Art_i == 0.

Lemma: Art_i == 0 under the given constraints.

Proof: the following three constraints are sufficient.

• ( ( 0 < ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) )
• ( ( 0 <= Art_i ) )
• ( ( ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) <= 0 ) )

With Art_i == 0 established, the constraint in question reduces to ((0 <= Dai) andBool (Dai <= maxUInt256)). This is proven true by the following constraints:

• ( ( 0 <= Dai ) )
• ( ( Dai <= maxUInt256 ) )

6. ( ( 0 <= ( Debt + ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) ) andBool ( ( Debt + ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) <= maxUInt256 ) )

Using the previously-proven lemma that Art_i == 0, this constraint reduces to saying that Debt in the range of a uint256. This is proven by the following constraints:

• ( ( 0 <= Debt ) )
• ( ( Debt <= maxUInt256 ) )

7. ( ( minSInt256 <= Rate ) andBool ( Rate <= maxSInt256 ) )

This follows from the following constraints:

• ( ( minSInt256 <= Rate ) )
• ( ( Rate <= maxSInt256 ) )

8. ( ( minSInt256 <= Art_i ) andBool ( Art_i <= maxSInt256 ) )

This follows from Art_i == 0, as well as the following two constraints:

• ( ( minSInt256 <= Art_i ) )
• ( ( Art_i <= maxSInt256 ) )

9. ( ( minSInt256 <= ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) andBool ( ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) <= maxSInt256 ) )

This follows from Art_i == 0, as well as the following two constraints:

• ( ( minSInt256 <= ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) )
• ( ( ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) <= maxSInt256 ) )

We have now exhausted the sub-claims; they are all true, so andBooling them together cannot result in a falsehood. Thus the given set of claims is contradictory.

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

; (set-option :auto-config false)
; (set-option :smt.mbqi false)
; (set-option :smt.array.extensional false)

; int extra
(define-fun int_max ((x Int) (y Int)) Int (ite (< x y) y x))
(define-fun int_min ((x Int) (y Int)) Int (ite (< x y) x y))
(define-fun int_abs ((x Int)) Int (ite (< x 0) (- 0 x) x))

; bool to int
(define-fun smt_bool2int ((b Bool)) Int (ite b 1 0))

; ceil32
(define-fun ceil32 ((x Int)) Int ( * ( div ( + x 31 ) 32 ) 32 ) )

;; 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 WordStack)
(declare-fun asByteStack (Int WordStack) WordStack)
(declare-fun asWord (WordStack) Int)
(declare-fun buf (Int Int) WordStack)
(declare-fun sizeWordStack (WordStack) Int)
(declare-fun _dotWS () WordStack)
(declare-fun _plusWS_ (WordStack WordStack) WordStack)
(declare-fun _WS_ (Int WordStack) WordStack)
(declare-fun chop (Int) Int)
(declare-fun smt_keccak (WordStack) Int)
(declare-fun smt_nthbyteof (Int Int Int) Int)
(declare-fun smt_num0 (Int) Int)
(declare-fun smt_num1 (Int) Int)
(declare-fun sizeWordStackAux (WordStack Int) Int)
(assert (forall ((|R_I_359| Int)) (= (chop |R_I_359|) (mod |R_I_359| 115792089237316195423570985008687907853269984665640564039457584007913129639936))))
(assert (forall ((|R__0_397| WordStack)(|R__1_398| Int)) (= (>= (sizeWordStackAux |R__0_397| |R__1_398|) 0) true)))
(declare-fun |VGas_2499| () Int)
(declare-fun |Base_2493| () Int)
(declare-fun |Duty_2495| () Int)
(declare-fun |TIME_2498| () Int)
(declare-fun |Rho_2418| () Int)
(declare-fun |Art_i_2501| () Int)
(declare-fun |Rate_2497| () Int)
(declare-fun |ACCT_ID_balance_2393| () Int)
(declare-fun |VCallDepth_2505| () Int)
(declare-fun |ACCT_ID_2402| () Int)
(declare-fun |CALLER_ID_2510| () Int)
(declare-fun |ORIGIN_ID_2392| () Int)
(declare-fun |ECREC_BAL_2391| () Int)
(declare-fun |SHA256_BAL_2404| () Int)
(declare-fun |RIP160_BAL_2511| () Int)
(declare-fun |ID_BAL_2390| () Int)
(declare-fun |MODEXP_BAL_2398| () Int)
(declare-fun |ECADD_BAL_2503| () Int)
(declare-fun |ECMUL_BAL_2394| () Int)
(declare-fun |ECPAIRING_BAL_2502| () Int)
(declare-fun |ABI_ilk_2401| () Int)
(declare-fun |Vat_2419| () Int)
(declare-fun |Vow_2420| () Int)
(declare-fun |Dai_2416| () Int)
(declare-fun |Debt_2494| () Int)
(declare-fun |Ilk_spot_2397| () Int)
(declare-fun |Ilk_line_2396| () Int)
(declare-fun |Ilk_dust_2395| () Int)
(declare-fun |Vat_balance_2504| () Int)
(declare-fun |CD_2405| () WordStack)
(assert (and
	(= (>= (- |VGas_2499| (+ (ite (= (+ |Base_2493| |Duty_2495|) 0) (+ 82 (ite (= (- |TIME_2498| |Rho_2418|) 0) 0 10)) (ite (= (mod (- |TIME_2498| |Rho_2418|) 2) 0) (ite (= (div (- |TIME_2498| |Rho_2418|) 2) 0) 150 (+ (* (- (smt_num0 (- |TIME_2498| |Rho_2418|)) 1) 172) (+ 437 (* (smt_num1 (- |TIME_2498| |Rho_2418|)) 287)))) (ite (= (div (- |TIME_2498| |Rho_2418|) 2) 0) 160 (+ (* (smt_num0 (- |TIME_2498| |Rho_2418|)) 172) (+ 447 (* (- (smt_num1 (- |TIME_2498| |Rho_2418|)) 1) 287)))))) (+ (ite (and (= |Rho_2418| 0) (not (= |TIME_2498| 0))) 15000 0) 38870))) 0) true)
	(= (<= (* |Art_i_2501| (- (div (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) |Rate_2497|) 1000000000000000000000000000) |Rate_2497|)) 0) true)
	(= (<= -57896044618658097711785492504343953926634992332820282019728792003956564819968 (* |Art_i_2501| (- (div (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) |Rate_2497|) 1000000000000000000000000000) |Rate_2497|))) true)
	(= (<= (* |Art_i_2501| (- (div (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) |Rate_2497|) 1000000000000000000000000000) |Rate_2497|)) 57896044618658097711785492504343953926634992332820282019728792003956564819967) true)
	(= (<= -57896044618658097711785492504343953926634992332820282019728792003956564819968 |Art_i_2501|) true)
	(= (<= |Art_i_2501| 57896044618658097711785492504343953926634992332820282019728792003956564819967) true)
	(= (< 0 (- (div (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) |Rate_2497|) 1000000000000000000000000000) |Rate_2497|)) true)
	(= (<= 0 (- (div (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) |Rate_2497|) 1000000000000000000000000000) |Rate_2497|)) true)
	(= (<= -57896044618658097711785492504343953926634992332820282019728792003956564819968 |Rate_2497|) true)
	(= (<= |Rate_2497| 57896044618658097711785492504343953926634992332820282019728792003956564819967) true)
	(= (<= 0 (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) |Rate_2497|)) true)
	(= (<= (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) |Rate_2497|) 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (= |Rate_2497| 0) false)
	(= (<= (+ |Base_2493| |Duty_2495|) 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (> 0 |ACCT_ID_balance_2393|) false)
	(= (>= |VCallDepth_2505| 1024) false)
	(= (<= |Rho_2418| |TIME_2498|) true)
	(= (<= 0 |ACCT_ID_2402|) true)
	(= (<= |ACCT_ID_2402| 1461501637330902918203684832716283019655932542975) true)
	(= (< 0 |ACCT_ID_2402|) true)
	(= (<= 9 |ACCT_ID_2402|) true)
	(= (<= 0 |CALLER_ID_2510|) true)
	(= (<= |CALLER_ID_2510| 1461501637330902918203684832716283019655932542975) true)
	(= (<= 0 |ORIGIN_ID_2392|) true)
	(= (<= |ORIGIN_ID_2392| 1461501637330902918203684832716283019655932542975) true)
	(= (<= 0 |TIME_2498|) true)
	(= (<= |TIME_2498| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |ACCT_ID_balance_2393|) true)
	(= (<= |ACCT_ID_balance_2393| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |ECREC_BAL_2391|) true)
	(= (<= |ECREC_BAL_2391| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |SHA256_BAL_2404|) true)
	(= (<= |SHA256_BAL_2404| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |RIP160_BAL_2511|) true)
	(= (<= |RIP160_BAL_2511| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |ID_BAL_2390|) true)
	(= (<= |ID_BAL_2390| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |MODEXP_BAL_2398|) true)
	(= (<= |MODEXP_BAL_2398| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |ECADD_BAL_2503|) true)
	(= (<= |ECADD_BAL_2503| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |ECMUL_BAL_2394|) true)
	(= (<= |ECMUL_BAL_2394| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |ECPAIRING_BAL_2502|) true)
	(= (<= |ECPAIRING_BAL_2502| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= |VCallDepth_2505| 1024) true)
	(= (<= 0 |ABI_ilk_2401|) true)
	(= (<= |ABI_ilk_2401| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |Vat_2419|) true)
	(= (<= |Vat_2419| 1461501637330902918203684832716283019655932542975) true)
	(= (<= 0 |Base_2493|) true)
	(= (<= |Base_2493| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |Vow_2420|) true)
	(= (<= |Vow_2420| 1461501637330902918203684832716283019655932542975) true)
	(= (<= 0 |Duty_2495|) true)
	(= (<= |Duty_2495| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |Rho_2418|) true)
	(= (<= |Rho_2418| 281474976710655) true)
	(= (<= 0 |Rate_2497|) true)
	(= (<= |Rate_2497| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |Art_i_2501|) true)
	(= (<= |Art_i_2501| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |Dai_2416|) true)
	(= (<= |Dai_2416| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |Debt_2494|) true)
	(= (<= |Debt_2494| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |Ilk_spot_2397|) true)
	(= (<= |Ilk_spot_2397| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |Ilk_line_2396|) true)
	(= (<= |Ilk_line_2396| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |Ilk_dust_2395|) true)
	(= (<= |Ilk_dust_2395| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= 0 |Vat_balance_2504|) true)
	(= (<= |Vat_balance_2504| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (<= (sizeWordStackAux |CD_2405| 0) 1250000000) true)
	(= (< 0 |Vat_2419|) true)
	(= (<= 9 |Vat_2419|) true)
	(= (< 0 |Vow_2420|) true)
	(= (<= 9 |Vow_2420|) true)
	(= (= |ACCT_ID_2402| |Vat_2419|) false)
	(= (>= (smt_num0 (- |TIME_2498| |Rho_2418|)) 0) true)
	(= (>= (smt_num1 (- |TIME_2498| |Rho_2418|)) 0) true)
	(= (<= 0 (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000)) true)
	(= (< (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) 1000000000000000000000000000) 115792089237316195423570985008687907853269984665640564039457584007913129639936) true)
	(= (>= |VGas_2499| (+ 300000000 (ite (= (+ |Base_2493| |Duty_2495|) 0) (+ 82 (ite (= (- |TIME_2498| |Rho_2418|) 0) 0 10)) (ite (= (mod (- |TIME_2498| |Rho_2418|) 2) 0) (ite (= (div (- |TIME_2498| |Rho_2418|) 2) 0) 150 (+ (* (- (smt_num0 (- |TIME_2498| |Rho_2418|)) 1) 172) (+ 437 (* (smt_num1 (- |TIME_2498| |Rho_2418|)) 287)))) (ite (= (div (- |TIME_2498| |Rho_2418|) 2) 0) 160 (+ (* (smt_num0 (- |TIME_2498| |Rho_2418|)) 172) (+ 447 (* (- (smt_num1 (- |TIME_2498| |Rho_2418|)) 1) 287)))))))) true)
	(= (and (< |VCallDepth_2505| 1024) (and (and (<= 0 (- |TIME_2498| |Rho_2418|)) (<= (- |TIME_2498| |Rho_2418|) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (<= 0 (+ |Base_2493| |Duty_2495|)) (<= (+ |Base_2493| |Duty_2495|) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (<= 0 (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) |Rate_2497|)) (<= (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) |Rate_2497|) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (<= 0 (+ |Dai_2416| (* |Art_i_2501| (- (div (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) |Rate_2497|) 1000000000000000000000000000) |Rate_2497|)))) (<= (+ |Dai_2416| (* |Art_i_2501| (- (div (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) |Rate_2497|) 1000000000000000000000000000) |Rate_2497|))) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (<= 0 (+ |Debt_2494| (* |Art_i_2501| (- (div (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) |Rate_2497|) 1000000000000000000000000000) |Rate_2497|)))) (<= (+ |Debt_2494| (* |Art_i_2501| (- (div (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) |Rate_2497|) 1000000000000000000000000000) |Rate_2497|))) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (<= -57896044618658097711785492504343953926634992332820282019728792003956564819968 |Rate_2497|) (<= |Rate_2497| 57896044618658097711785492504343953926634992332820282019728792003956564819967)) (and (and (<= -57896044618658097711785492504343953926634992332820282019728792003956564819968 |Art_i_2501|) (<= |Art_i_2501| 57896044618658097711785492504343953926634992332820282019728792003956564819967)) (and (<= -57896044618658097711785492504343953926634992332820282019728792003956564819968 (* |Art_i_2501| (- (div (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) |Rate_2497|) 1000000000000000000000000000) |Rate_2497|))) (<= (* |Art_i_2501| (- (div (* (smt_rpow 1000000000000000000000000000 (+ |Base_2493| |Duty_2495|) (- |TIME_2498| |Rho_2418|) 1000000000000000000000000000) |Rate_2497|) 1000000000000000000000000000) |Rate_2497|)) 57896044618658097711785492504343953926634992332820282019728792003956564819967)))))))))) false)
	(= (<= 0 (+ |Base_2493| |Duty_2495|)) true)
	(= (<= 0 (- |TIME_2498| |Rho_2418|)) true)
	(= (<= (- |TIME_2498| |Rho_2418|) 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
	(= (< 0 (- |VGas_2499| (+ 5013 (ite (= (+ |Base_2493| |Duty_2495|) 0) (+ 82 (ite (= (- |TIME_2498| |Rho_2418|) 0) 0 10)) (ite (= (mod (- |TIME_2498| |Rho_2418|) 2) 0) (ite (= (div (- |TIME_2498| |Rho_2418|) 2) 0) 150 (+ (* (- (smt_num0 (- |TIME_2498| |Rho_2418|)) 1) 172) (+ 437 (* (smt_num1 (- |TIME_2498| |Rho_2418|)) 287)))) (ite (= (div (- |TIME_2498| |Rho_2418|) 2) 0) 160 (+ (* (smt_num0 (- |TIME_2498| |Rho_2418|)) 172) (+ 447 (* (- (smt_num1 (- |TIME_2498| |Rho_2418|)) 1) 287))))))))) true)))
(check-sat)