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.

Spec for proof:

requires "../rules.k"
requires "../bin_runtime.k"

module EE6BB295DCB91641336938CC51CD46661611B52DF7C232B21F4F14DAEEE5DABD
  imports ETHEREUM-SIMULATION
  imports EVM
  imports RULES
  imports BIN_RUNTIME

// Jug_drip
rule [Jug.drip.fail.rough]:
  <k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k>
  <exit-code> 1 </exit-code>
  <mode> NORMAL </mode>
  <schedule> PETERSBURG </schedule>
  <ethereum>
    <evm>
      <output> _ => _ </output>
      <statusCode> _ => FAILURE:EndStatusCode </statusCode>
      <callStack> VCallStack </callStack>
      <interimStates> _ </interimStates>
      <touchedAccounts> _ => _ </touchedAccounts>
      <callState>
        <program> #asMapOpCodes(#dasmOpCodes(Jug_bin_runtime, PETERSBURG)) </program>
        <programBytes> Jug_bin_runtime </programBytes>
        <id> ACCT_ID </id>
        <caller> CALLER_ID </caller>
        <callData> #abiCallData("drip", #bytes32(ABI_ilk)) ++ CD => _ </callData>
        <callValue> VCallValue </callValue>
        <wordStack> .WordStack => _ </wordStack>
        <localMem> .Map => _ </localMem>
        <pc> 0 => _ </pc>
        <gas> VGas => _ </gas>
        <memoryUsed> 0 => _ </memoryUsed>
        <callGas> _ => _ </callGas>
        <static> false </static>
        <callDepth> VCallDepth => _ </callDepth>
      </callState>
      <substate>
        <selfDestruct> VSelfDestruct </selfDestruct>
        <log> _ => VLog </log>
        <refund> _ => VRefund </refund>
      </substate>
      <gasPrice> _ </gasPrice>
      <origin> ORIGIN_ID </origin>
      <previousHash> _ </previousHash>
      <ommersHash> _ </ommersHash>
      <coinbase> _ </coinbase>
      <stateRoot> _ </stateRoot>
      <transactionsRoot> _ </transactionsRoot>
      <receiptsRoot> _ </receiptsRoot>
      <logsBloom> _ </logsBloom>
      <difficulty> _ </difficulty>
      <number> _ </number>
      <gasLimit> _ </gasLimit>
      <gasUsed> _ </gasUsed>
      <timestamp> TIME </timestamp>
      <extraData> _ </extraData>
      <mixHash> _ </mixHash>
      <blockNonce> _ </blockNonce>
      <ommerBlockHeaders> _ </ommerBlockHeaders>
      <blockhash> _ </blockhash>
    </evm>
    <network>
      <activeAccounts> SetItem(ACCT_ID)
      SetItem(Vat)
      SetItem(1)
      SetItem(2)
      SetItem(3)
      SetItem(4)
      SetItem(5)
      SetItem(6)
      SetItem(7)
      SetItem(8) _ </activeAccounts>
      <accounts>
        <account>
          <acctID> ACCT_ID </acctID>
          <balance> ACCT_ID_balance </balance>
          <code> Jug_bin_runtime </code>
          <storage>         
           .Map 
          [#Jug.vat <- (Vat  => _)]        
          [#Jug.vow <- (Vow  => _)]        
          [#Jug.base <- (Base => _)]        
          [#Jug.ilks[ABI_ilk].duty <- (Duty => _)]        
          [#Jug.ilks[ABI_ilk].rho <- (Rho  => _)]
            _:Map 
           </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> Vat </acctID>
          <balance> Vat_balance </balance>
          <code> Vat_bin_runtime </code>
          <storage>         
           .Map 
          [#Vat.live <- (Live     => _)]        
          [#Vat.wards[ACCT_ID] <- (May      => _)]        
          [#Vat.ilks[ABI_ilk].rate <- (Rate     => _)]        
          [#Vat.ilks[ABI_ilk].Art <- (Art_i    => _)]        
          [#Vat.ilks[ABI_ilk].spot <- (Ilk_spot => _)]        
          [#Vat.ilks[ABI_ilk].line <- (Ilk_line => _)]        
          [#Vat.ilks[ABI_ilk].dust <- (Ilk_dust => _)]        
          [#Vat.dai[Vow] <- (Dai      => _)]        
          [#Vat.debt <- (Debt     => _)]
            _:Map 
           </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 1 </acctID>
          <balance> ECREC_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 2 </acctID>
          <balance> SHA256_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 3 </acctID>
          <balance> RIP160_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 4 </acctID>
          <balance> ID_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 5 </acctID>
          <balance> MODEXP_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 6 </acctID>
          <balance> ECADD_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 7 </acctID>
          <balance> ECMUL_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 8 </acctID>
          <balance> ECPAIRING_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
       ... 
      </accounts>
      <txOrder> _ </txOrder>
      <txPending> _ </txPending>
      <messages> _ </messages>
    </network>
  </ethereum>
requires #rangeAddress(ACCT_ID)
andBool #notPrecompileAddress(ACCT_ID)
andBool #rangeAddress(CALLER_ID)
andBool #rangeAddress(ORIGIN_ID)
andBool #rangeUInt(256, TIME)
andBool #rangeUInt(256, ACCT_ID_balance)
andBool #rangeUInt(256, ECREC_BAL)
andBool #rangeUInt(256, SHA256_BAL)
andBool #rangeUInt(256, RIP160_BAL)
andBool #rangeUInt(256, ID_BAL)
andBool #rangeUInt(256, MODEXP_BAL)
andBool #rangeUInt(256, ECADD_BAL)
andBool #rangeUInt(256, ECMUL_BAL)
andBool #rangeUInt(256, ECPAIRING_BAL)
andBool VCallDepth <=Int 1024
andBool #rangeUInt(256, VCallValue)

  andBool (#rangeBytes(32, ABI_ilk)
  andBool (#rangeAddress(Vat)
  andBool (#rangeUInt(256, Base)
  andBool (#rangeAddress(Vow)
  andBool (#rangeUInt(256, Duty)
  andBool (#rangeUInt(48, Rho)
  andBool (#rangeUInt(256, May)
  andBool (#rangeUInt(256, Rate)
  andBool (#rangeUInt(256, Art_i)
  andBool (#rangeUInt(256, Dai)
  andBool (#rangeUInt(256, Debt)
  andBool (#rangeUInt(256, Ilk_spot)
  andBool (#rangeUInt(256, Ilk_line)
  andBool (#rangeUInt(256, Ilk_dust)
  andBool (#rangeUInt(256, Vat_balance)
  andBool ((#sizeWordStack(CD) <=Int 1250000000)
  andBool ((#notPrecompileAddress(Vat))
  andBool ((#notPrecompileAddress(Vow))
  andBool ((ACCT_ID =/=Int Vat)
  andBool ((num0(TIME -Int Rho) >=Int 0)
  andBool ((num1(TIME -Int Rho) >=Int 0)
  andBool ((0 <=Int #rpow(#Ray, Base +Int Duty, TIME -Int Rho, #Ray))
  andBool ((#rpow(#Ray, Base +Int Duty, TIME -Int Rho, #Ray) *Int #Ray <Int pow256)
  andBool (VGas >=Int 300000000 +Int ((#if ( (Base +Int Duty) ==K 0 ) #then (#if ( (TIME -Int Rho) ==K 0 ) #then 82 #else 92 #fi) #else (#if ( ( (TIME -Int Rho) modInt 2 ) ==K 0 ) #then (#if ( ( (TIME -Int Rho) /Int 2 ) ==K 0 ) #then 150 #else ( 437 +Int ( ( ( num0(TIME -Int Rho) -Int 1 ) *Int 172 ) +Int ( num1(TIME -Int Rho) *Int 287 ) ) ) #fi) #else (#if ( ( (TIME -Int Rho) /Int 2 ) ==K 0 ) #then 160 #else ( 447 +Int ( ( num0(TIME -Int Rho) *Int 172 ) +Int ( ( num1(TIME -Int Rho) -Int 1 ) *Int 287 ) ) ) #fi) #fi) #fi))))))))))))))))))))))))))
  andBool notBool (
    ((((VCallValue:Int ==Int 0)))
    andBool ((((VCallDepth:Int <Int 1024)))
    andBool ((((May:Int ==Int 1)))
    andBool ((((Live ==Int 1)))
    andBool (((#rangeUInt(256, TIME:Int -Int Rho:Int)))
    andBool (((#rangeUInt(256, Base:Int +Int Duty:Int)))
    andBool (((#rangeUInt(256, #rpow(#Ray, Base:Int +Int Duty:Int, TIME:Int -Int Rho:Int, #Ray) *Int Rate:Int)))
    andBool (((#rangeUInt(256, Dai:Int  +Int Art_i:Int *Int (#rmul(#rpow(#Ray, Base:Int +Int Duty:Int, TIME:Int -Int Rho:Int, #Ray), Rate:Int) -Int Rate:Int))))
    andBool (((#rangeUInt(256, Debt:Int +Int Art_i:Int *Int (#rmul(#rpow(#Ray, Base:Int +Int Duty:Int, TIME:Int -Int Rho:Int, #Ray), Rate:Int) -Int Rate:Int))))
    andBool ((#rangeSInt(256, Rate:Int))
    andBool ((#rangeSInt(256, Art_i:Int))
    andBool ((#rangeSInt(256, Art_i:Int *Int (#rmul(#rpow(#Ray, Base:Int +Int Duty:Int, TIME:Int -Int Rho:Int, #Ray), Rate:Int) -Int Rate:Int)))))))))))))))
  ) 
ensures
FAILURE =/=K EVMC_SUCCESS

// Jug_adduu
rule [Jug.adduu.pass]:
  <k> #execute ~> CONTINUATION => #execute ~> CONTINUATION </k>
  <exit-code> 1 </exit-code>
  <mode> NORMAL </mode>
  <schedule> PETERSBURG </schedule>
  <ethereum>
    <evm>
      <output> VOutput => VOutput </output>
      <statusCode> _ => _ </statusCode>
      <callStack> VCallStack </callStack>
      <interimStates> _ </interimStates>
      <touchedAccounts> _ => _ </touchedAccounts>
      <callState>
        <program> #asMapOpCodes(#dasmOpCodes(Jug_bin_runtime, PETERSBURG)) </program>
        <programBytes> Jug_bin_runtime </programBytes>
        <id> ACCT_ID </id>
        <caller> CALLER_ID </caller>
        <callData> _ => _ </callData>
        <callValue> VCallValue </callValue>
        <wordStack> ABI_y : ABI_x : JMPTO : WS  =>  JMPTO : ABI_x +Int ABI_y : WS </wordStack>
        <localMem> _ </localMem>
        <pc> 4288 => 4313 </pc>
        <gas> VGas => ( VGas -Int 54 ) </gas>
        <memoryUsed> VMemoryUsed </memoryUsed>
        <callGas> _ => _ </callGas>
        <static> _ </static>
        <callDepth> VCallDepth </callDepth>
      </callState>
      <substate>
        <selfDestruct> VSelfDestruct </selfDestruct>
        <log> _ => VLog </log>
        <refund> _ => VRefund </refund>
      </substate>
      <gasPrice> _ </gasPrice>
      <origin> ORIGIN_ID </origin>
      <previousHash> _ </previousHash>
      <ommersHash> _ </ommersHash>
      <coinbase> _ </coinbase>
      <stateRoot> _ </stateRoot>
      <transactionsRoot> _ </transactionsRoot>
      <receiptsRoot> _ </receiptsRoot>
      <logsBloom> _ </logsBloom>
      <difficulty> _ </difficulty>
      <number> _ </number>
      <gasLimit> _ </gasLimit>
      <gasUsed> _ </gasUsed>
      <timestamp> TIME </timestamp>
      <extraData> _ </extraData>
      <mixHash> _ </mixHash>
      <blockNonce> _ </blockNonce>
      <ommerBlockHeaders> _ </ommerBlockHeaders>
      <blockhash> _ </blockhash>
    </evm>
    <network>
      <activeAccounts> SetItem(ACCT_ID)
      SetItem(1)
      SetItem(2)
      SetItem(3)
      SetItem(4)
      SetItem(5)
      SetItem(6)
      SetItem(7)
      SetItem(8) _ </activeAccounts>
      <accounts>
        <account>
          <acctID> ACCT_ID </acctID>
          <balance> ACCT_ID_balance </balance>
          <code> Jug_bin_runtime </code>
          <storage>         
           .Map 
          
            _:Map 
           </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 1 </acctID>
          <balance> ECREC_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 2 </acctID>
          <balance> SHA256_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 3 </acctID>
          <balance> RIP160_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 4 </acctID>
          <balance> ID_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 5 </acctID>
          <balance> MODEXP_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 6 </acctID>
          <balance> ECADD_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 7 </acctID>
          <balance> ECMUL_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 8 </acctID>
          <balance> ECPAIRING_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
       ... 
      </accounts>
      <txOrder> _ </txOrder>
      <txPending> _ </txPending>
      <messages> _ </messages>
    </network>
  </ethereum>
requires #rangeAddress(ACCT_ID)
andBool #notPrecompileAddress(ACCT_ID)
andBool #rangeAddress(CALLER_ID)
andBool #rangeAddress(ORIGIN_ID)
andBool #rangeUInt(256, TIME)
andBool #rangeUInt(256, ACCT_ID_balance)
andBool #rangeUInt(256, ECREC_BAL)
andBool #rangeUInt(256, SHA256_BAL)
andBool #rangeUInt(256, RIP160_BAL)
andBool #rangeUInt(256, ID_BAL)
andBool #rangeUInt(256, MODEXP_BAL)
andBool #rangeUInt(256, ECADD_BAL)
andBool #rangeUInt(256, ECMUL_BAL)
andBool #rangeUInt(256, ECPAIRING_BAL)
andBool VCallDepth <=Int 1024
andBool #rangeUInt(256, VCallValue)

  andBool (#rangeUInt(256, ABI_x)
  andBool (#rangeUInt(256, ABI_y)
  andBool ((#sizeWordStack(WS) <=Int 100)
  andBool (#rangeUInt(256, VMemoryUsed)
  andBool (0 <Int ( VGas -Int 54 )
  andBool ((#rangeUInt(256, ABI_x +Int ABI_y)))))))) 
[trusted]


// Jug_rpow
rule [Jug.rpow.pass]:
  <k> #execute ~> CONTINUATION => #execute ~> CONTINUATION </k>
  <exit-code> 1 </exit-code>
  <mode> NORMAL </mode>
  <schedule> PETERSBURG </schedule>
  <ethereum>
    <evm>
      <output> VOutput => VOutput </output>
      <statusCode> _ => _ </statusCode>
      <callStack> VCallStack </callStack>
      <interimStates> _ </interimStates>
      <touchedAccounts> _ => _ </touchedAccounts>
      <callState>
        <program> #asMapOpCodes(#dasmOpCodes(Jug_bin_runtime, PETERSBURG)) </program>
        <programBytes> Jug_bin_runtime </programBytes>
        <id> ACCT_ID </id>
        <caller> CALLER_ID </caller>
        <callData> _ => _ </callData>
        <callValue> VCallValue </callValue>
        <wordStack> ABI_b : ABI_n : ABI_x : JMPTO : WS  =>  JMPTO : #rpow(ABI_b, ABI_x, ABI_n, ABI_b) : WS </wordStack>
        <localMem> _ </localMem>
        <pc> 4314 => 4511 </pc>
        <gas> VGas => VGas -Int ((#if ( ABI_x ==K 0 ) #then (#if ( ABI_n ==K 0 ) #then 82 #else 92 #fi) #else (#if ( ( ABI_n modInt 2 ) ==K 0 ) #then (#if ( ( ABI_n /Int 2 ) ==K 0 ) #then 150 #else ( 437 +Int ( ( ( num0(ABI_n) -Int 1 ) *Int 172 ) +Int ( num1(ABI_n) *Int 287 ) ) ) #fi) #else (#if ( ( ABI_n /Int 2 ) ==K 0 ) #then 160 #else ( 447 +Int ( ( num0(ABI_n) *Int 172 ) +Int ( ( num1(ABI_n) -Int 1 ) *Int 287 ) ) ) #fi) #fi) #fi)) </gas>
        <memoryUsed> VMemoryUsed </memoryUsed>
        <callGas> _ => _ </callGas>
        <static> _ </static>
        <callDepth> VCallDepth </callDepth>
      </callState>
      <substate>
        <selfDestruct> VSelfDestruct </selfDestruct>
        <log> _ => VLog </log>
        <refund> _ => VRefund </refund>
      </substate>
      <gasPrice> _ </gasPrice>
      <origin> ORIGIN_ID </origin>
      <previousHash> _ </previousHash>
      <ommersHash> _ </ommersHash>
      <coinbase> _ </coinbase>
      <stateRoot> _ </stateRoot>
      <transactionsRoot> _ </transactionsRoot>
      <receiptsRoot> _ </receiptsRoot>
      <logsBloom> _ </logsBloom>
      <difficulty> _ </difficulty>
      <number> _ </number>
      <gasLimit> _ </gasLimit>
      <gasUsed> _ </gasUsed>
      <timestamp> TIME </timestamp>
      <extraData> _ </extraData>
      <mixHash> _ </mixHash>
      <blockNonce> _ </blockNonce>
      <ommerBlockHeaders> _ </ommerBlockHeaders>
      <blockhash> _ </blockhash>
    </evm>
    <network>
      <activeAccounts> SetItem(ACCT_ID)
      SetItem(1)
      SetItem(2)
      SetItem(3)
      SetItem(4)
      SetItem(5)
      SetItem(6)
      SetItem(7)
      SetItem(8) _ </activeAccounts>
      <accounts>
        <account>
          <acctID> ACCT_ID </acctID>
          <balance> ACCT_ID_balance </balance>
          <code> Jug_bin_runtime </code>
          <storage>         
           .Map 
          
            _:Map 
           </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 1 </acctID>
          <balance> ECREC_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 2 </acctID>
          <balance> SHA256_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 3 </acctID>
          <balance> RIP160_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 4 </acctID>
          <balance> ID_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 5 </acctID>
          <balance> MODEXP_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 6 </acctID>
          <balance> ECADD_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 7 </acctID>
          <balance> ECMUL_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 8 </acctID>
          <balance> ECPAIRING_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
       ... 
      </accounts>
      <txOrder> _ </txOrder>
      <txPending> _ </txPending>
      <messages> _ </messages>
    </network>
  </ethereum>
requires #rangeAddress(ACCT_ID)
andBool #notPrecompileAddress(ACCT_ID)
andBool #rangeAddress(CALLER_ID)
andBool #rangeAddress(ORIGIN_ID)
andBool #rangeUInt(256, TIME)
andBool #rangeUInt(256, ACCT_ID_balance)
andBool #rangeUInt(256, ECREC_BAL)
andBool #rangeUInt(256, SHA256_BAL)
andBool #rangeUInt(256, RIP160_BAL)
andBool #rangeUInt(256, ID_BAL)
andBool #rangeUInt(256, MODEXP_BAL)
andBool #rangeUInt(256, ECADD_BAL)
andBool #rangeUInt(256, ECMUL_BAL)
andBool #rangeUInt(256, ECPAIRING_BAL)
andBool VCallDepth <=Int 1024
andBool #rangeUInt(256, VCallValue)

  andBool (#rangeUInt(256, ABI_x)
  andBool (#rangeUInt(256, ABI_n)
  andBool (#rangeUInt(256, ABI_b)
  andBool ((#sizeWordStack(WS) <=Int 999)
  andBool ((num0(ABI_n) >=Int 0)
  andBool ((num1(ABI_n) >=Int 0)
  andBool ((ABI_b =/=Int 0)
  andBool ((0 <=Int #rpow(ABI_b, ABI_x, ABI_n, ABI_b))
  andBool ((#rpow(ABI_b, ABI_x, ABI_n, ABI_b) *Int ABI_b <Int pow256)
  andBool (#rangeUInt(256, VMemoryUsed)
  andBool (0 <Int VGas -Int ((#if ( ABI_x ==K 0 ) #then (#if ( ABI_n ==K 0 ) #then 82 #else 92 #fi) #else (#if ( ( ABI_n modInt 2 ) ==K 0 ) #then (#if ( ( ABI_n /Int 2 ) ==K 0 ) #then 150 #else ( 437 +Int ( ( ( num0(ABI_n) -Int 1 ) *Int 172 ) +Int ( num1(ABI_n) *Int 287 ) ) ) #fi) #else (#if ( ( ABI_n /Int 2 ) ==K 0 ) #then 160 #else ( 447 +Int ( ( num0(ABI_n) *Int 172 ) +Int ( ( num1(ABI_n) -Int 1 ) *Int 287 ) ) ) #fi) #fi) #fi))))))))))))) 
[trusted]


// Vat_fold
rule [Vat.fold.pass]:
  <k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k>
  <exit-code> 1 </exit-code>
  <mode> NORMAL </mode>
  <schedule> PETERSBURG </schedule>
  <ethereum>
    <evm>
      <output> .WordStack </output>
      <statusCode> _ => EVMC_SUCCESS </statusCode>
      <callStack> VCallStack </callStack>
      <interimStates> _ </interimStates>
      <touchedAccounts> _ => _ </touchedAccounts>
      <callState>
        <program> #asMapOpCodes(#dasmOpCodes(Vat_bin_runtime, PETERSBURG)) </program>
        <programBytes> Vat_bin_runtime </programBytes>
        <id> ACCT_ID </id>
        <caller> CALLER_ID </caller>
        <callData> #abiCallData("fold", #bytes32(ABI_i), #address(ABI_u), #int256(ABI_rate)) ++ CD => _ </callData>
        <callValue> VCallValue </callValue>
        <wordStack> .WordStack => _ </wordStack>
        <localMem> .Map => _ </localMem>
        <pc> 0 => _ </pc>
        <gas> VGas => ( VGas -Int ( (#if ( ( ( 0 <=Int ABI_rate ) ==K true ) andBool ( ( ABI_rate <=Int 0 ) ==K true ) ) #then 0 #else 14 #fi) +Int ( (#if ( ( Rate_i ==K 0 ) andBool (notBool ( ( Rate_i +Int ABI_rate ) ==K 0 ) ) ) #then 15000 #else 0 #fi) +Int ( (#if ( ABI_rate ==K 0 ) #then 0 #else 36 #fi) +Int ( (#if ( ( ( 0 <=Int ( Art_i *Int ABI_rate ) ) ==K true ) andBool ( ( ( Art_i *Int ABI_rate ) <=Int 0 ) ==K true ) ) #then 0 #else 14 #fi) +Int ( (#if ( ( Dai_u ==K 0 ) andBool (notBool ( ( Dai_u +Int ( Art_i *Int ABI_rate ) ) ==K 0 ) ) ) #then 15000 #else 0 #fi) +Int ( (#if ( ( ( 0 <=Int ( Art_i *Int ABI_rate ) ) ==K true ) andBool ( ( ( Art_i *Int ABI_rate ) <=Int 0 ) ==K true ) ) #then 0 #else 14 #fi) +Int ( (#if ( ( Debt ==K 0 ) andBool (notBool ( ( Debt +Int ( Art_i *Int ABI_rate ) ) ==K 0 ) ) ) #then 15000 #else 0 #fi) +Int 21932 ) ) ) ) ) ) ) ) </gas>
        <memoryUsed> 0 => _ </memoryUsed>
        <callGas> _ => _ </callGas>
        <static> false </static>
        <callDepth> VCallDepth </callDepth>
      </callState>
      <substate>
        <selfDestruct> VSelfDestruct </selfDestruct>
        <log> _ => VLog </log>
        <refund> _ => VRefund </refund>
      </substate>
      <gasPrice> _ </gasPrice>
      <origin> ORIGIN_ID </origin>
      <previousHash> _ </previousHash>
      <ommersHash> _ </ommersHash>
      <coinbase> _ </coinbase>
      <stateRoot> _ </stateRoot>
      <transactionsRoot> _ </transactionsRoot>
      <receiptsRoot> _ </receiptsRoot>
      <logsBloom> _ </logsBloom>
      <difficulty> _ </difficulty>
      <number> _ </number>
      <gasLimit> _ </gasLimit>
      <gasUsed> _ </gasUsed>
      <timestamp> TIME </timestamp>
      <extraData> _ </extraData>
      <mixHash> _ </mixHash>
      <blockNonce> _ </blockNonce>
      <ommerBlockHeaders> _ </ommerBlockHeaders>
      <blockhash> _ </blockhash>
    </evm>
    <network>
      <activeAccounts> SetItem(ACCT_ID)
      SetItem(1)
      SetItem(2)
      SetItem(3)
      SetItem(4)
      SetItem(5)
      SetItem(6)
      SetItem(7)
      SetItem(8) _ </activeAccounts>
      <accounts>
        <account>
          <acctID> ACCT_ID </acctID>
          <balance> ACCT_ID_balance </balance>
          <code> Vat_bin_runtime </code>
          <storage>         
           .Map 
          [#Vat.wards[CALLER_ID] <- (May    => May)]        
          [#Vat.ilks[ABI_i].rate <- (Rate_i => Rate_i +Int ABI_rate)]        
          [#Vat.ilks[ABI_i].Art <- (Art_i  => Art_i)]        
          [#Vat.dai[ABI_u] <- (Dai_u  => Dai_u +Int Art_i *Int ABI_rate)]        
          [#Vat.debt <- (Debt   => Debt  +Int Art_i *Int ABI_rate)]        
          [#Vat.live <- (Live   => Live)]
            _:Map 
           </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 1 </acctID>
          <balance> ECREC_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 2 </acctID>
          <balance> SHA256_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 3 </acctID>
          <balance> RIP160_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 4 </acctID>
          <balance> ID_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 5 </acctID>
          <balance> MODEXP_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 6 </acctID>
          <balance> ECADD_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 7 </acctID>
          <balance> ECMUL_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
        <account>
          <acctID> 8 </acctID>
          <balance> ECPAIRING_BAL </balance>
          <code> .WordStack </code>
          <storage> _:Map </storage>
          <origStorage> _ </origStorage>
          <nonce> _ </nonce>
        </account>
       ... 
      </accounts>
      <txOrder> _ </txOrder>
      <txPending> _ </txPending>
      <messages> _ </messages>
    </network>
  </ethereum>
requires #rangeAddress(ACCT_ID)
andBool #notPrecompileAddress(ACCT_ID)
andBool #rangeAddress(CALLER_ID)
andBool #rangeAddress(ORIGIN_ID)
andBool #rangeUInt(256, TIME)
andBool #rangeUInt(256, ACCT_ID_balance)
andBool #rangeUInt(256, ECREC_BAL)
andBool #rangeUInt(256, SHA256_BAL)
andBool #rangeUInt(256, RIP160_BAL)
andBool #rangeUInt(256, ID_BAL)
andBool #rangeUInt(256, MODEXP_BAL)
andBool #rangeUInt(256, ECADD_BAL)
andBool #rangeUInt(256, ECMUL_BAL)
andBool #rangeUInt(256, ECPAIRING_BAL)
andBool VCallDepth <=Int 1024
andBool #rangeUInt(256, VCallValue)

  andBool (#rangeBytes(32, ABI_i)
  andBool (#rangeAddress(ABI_u)
  andBool (#rangeSInt(256, ABI_rate)
  andBool (#rangeUInt(256, May)
  andBool (#rangeUInt(256, Rate_i)
  andBool (#rangeUInt(256, Dai_u)
  andBool (#rangeUInt(256, Art_i)
  andBool (#rangeUInt(256, Debt)
  andBool (#sizeWordStack(CD) <=Int 1250000000
  andBool (0 <Int ( VGas -Int ( (#if ( ( ( 0 <=Int ABI_rate ) ==K true ) andBool ( ( ABI_rate <=Int 0 ) ==K true ) ) #then 0 #else 14 #fi) +Int ( (#if ( ( Rate_i ==K 0 ) andBool (notBool ( ( Rate_i +Int ABI_rate ) ==K 0 ) ) ) #then 15000 #else 0 #fi) +Int ( (#if ( ABI_rate ==K 0 ) #then 0 #else 36 #fi) +Int ( (#if ( ( ( 0 <=Int ( Art_i *Int ABI_rate ) ) ==K true ) andBool ( ( ( Art_i *Int ABI_rate ) <=Int 0 ) ==K true ) ) #then 0 #else 14 #fi) +Int ( (#if ( ( Dai_u ==K 0 ) andBool (notBool ( ( Dai_u +Int ( Art_i *Int ABI_rate ) ) ==K 0 ) ) ) #then 15000 #else 0 #fi) +Int ( (#if ( ( ( 0 <=Int ( Art_i *Int ABI_rate ) ) ==K true ) andBool ( ( ( Art_i *Int ABI_rate ) <=Int 0 ) ==K true ) ) #then 0 #else 14 #fi) +Int ( (#if ( ( Debt ==K 0 ) andBool (notBool ( ( Debt +Int ( Art_i *Int ABI_rate ) ) ==K 0 ) ) ) #then 15000 #else 0 #fi) +Int 21932 ) ) ) ) ) ) ) )
  andBool ((((VCallValue ==Int 0)))
  andBool ((((May ==Int 1)))
  andBool ((((Live ==Int 1)))
  andBool ((((Art_i <=Int maxSInt256)))
  andBool (((#rangeSInt(256, Art_i *Int ABI_rate)))
  andBool ((#rangeUInt(256, Rate_i +Int ABI_rate))
  andBool ((#rangeUInt(256, Dai_u  +Int (Art_i *Int ABI_rate)))
  andBool ((#rangeUInt(256, Debt   +Int (Art_i *Int ABI_rate))))))))))))))))))))) 
[trusted]


endmodule

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