Skip to content

Instantly share code, notes, and snippets.

@ngmachado

ngmachado/erc20_stream_core.smt.report.md

Created February 19, 2026 19:29
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save ngmachado/4bb940bbe5c8e68c5dc137acffe36d71 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save ngmachado/4bb940bbe5c8e68c5dc137acffe36d71 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
erc20_stream_core.smt.report.md

SMT Encoding Report

1. Run Metadata

  • Source file: /Users/logic/Ora/Ora/ora-example/apps/erc20_stream_core.ora
  • Generated at (unix): 1771529158
  • Verification mode: full
  • verify_calls: true
  • verify_state: true
  • parallel: true
  • timeout_ms: 60000

2. Summary

  • Total queries: 60
  • SAT: 12
  • UNSAT: 48
  • UNKNOWN: 0
  • Failed obligations: 0
  • Inconsistent assumption bases: 0
  • Proven guards: 2
  • Violatable guards: 0
  • Verification success: true
  • Verification errors: 0
  • Verification diagnostics: 0

3. Query Kind Counts

  • base: 10
  • obligation: 46
  • loop_invariant_step: 0
  • loop_invariant_post: 0
  • guard_satisfy: 2
  • guard_violate: 2

4. Findings

  • No verification findings.

5. Query Catalog

Q1 - base

  • Function: claim
  • Location: loc("erc20_stream_core.ora":270:0
  • Status: SAT
  • Elapsed ms: 0
  • SMT-LIB:


Q2 - obligation


    

  • Function: claim
    • 

  • Location: loc("erc20_stream_core.ora":293:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 31
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577248 () (_ BitVec 160))
(declare-fun v_40656577200 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_recipient () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577296 () (_ BitVec 256))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644503568 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644504688 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577248 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577200) true true))
(assert (xor (not (= (select g_stream_recipient v_40656577200) v_40656577248)) true))
(assert (xor (bvule (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
            (select g_stream_claimed v_40656577200))
     true))
(assert (= (ora.field.value struct_init_40644503568)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644503568)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (ora.field.overflow struct_init_40644503568) true))
(assert (= (ora.field.value struct_init_40644504688)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644504688)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (bvugt (ora.field.value struct_init_40644504688)
            (select g_stream_deposit v_40656577200))
     true))
(assert (not (xor (bvult (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_claimed v_40656577200))
          true)))



Q3 - obligation


    

  • Function: claim
    • 

  • Location: loc("erc20_stream_core.ora":297:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577248 () (_ BitVec 160))
(declare-fun v_40656577200 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_recipient () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577296 () (_ BitVec 256))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644503568 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644504688 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577248 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577200) true true))
(assert (xor (not (= (select g_stream_recipient v_40656577200) v_40656577248)) true))
(assert (xor (bvule (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
            (select g_stream_claimed v_40656577200))
     true))
(assert (= (ora.field.value struct_init_40644503568)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644503568)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (ora.field.overflow struct_init_40644503568) true))
(assert (= (ora.field.value struct_init_40644504688)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644504688)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (bvugt (ora.field.value struct_init_40644504688)
            (select g_stream_deposit v_40656577200))
     true))
(assert (xor (bvult g_total_escrowed
            (bvsub (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                   (select g_stream_claimed v_40656577200)))
     true))
(assert (let ((a!1 (xor (bvult #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                       (bvsub (accruedAt_6129c65b415ce3b8_r0
                                v_40656577200
                                v_40656577296)
                              (select g_stream_claimed v_40656577200)))
                true)))
  (not a!1)))



Q4 - obligation


    

  • Function: claim
    • 

  • Location: loc("erc20_stream_core.ora":297:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577248 () (_ BitVec 160))
(declare-fun v_40656577200 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_recipient () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577296 () (_ BitVec 256))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644503568 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644504688 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577248 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577200) true true))
(assert (xor (not (= (select g_stream_recipient v_40656577200) v_40656577248)) true))
(assert (xor (bvule (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
            (select g_stream_claimed v_40656577200))
     true))
(assert (= (ora.field.value struct_init_40644503568)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644503568)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (ora.field.overflow struct_init_40644503568) true))
(assert (= (ora.field.value struct_init_40644504688)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644504688)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (bvugt (ora.field.value struct_init_40644504688)
            (select g_stream_deposit v_40656577200))
     true))
(assert (xor (bvult g_total_escrowed
            (bvsub (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                   (select g_stream_claimed v_40656577200)))
     true))
(assert (let ((a!1 (xor (bvult #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                       (bvsub (accruedAt_6129c65b415ce3b8_r0
                                v_40656577200
                                v_40656577296)
                              (select g_stream_claimed v_40656577200)))
                true)))
  (not a!1)))



Q5 - obligation


    

  • Function: claim
    • 

  • Location: loc("erc20_stream_core.ora":297:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577248 () (_ BitVec 160))
(declare-fun v_40656577200 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_recipient () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577296 () (_ BitVec 256))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644503568 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644504688 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577248 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577200) true true))
(assert (xor (not (= (select g_stream_recipient v_40656577200) v_40656577248)) true))
(assert (xor (bvule (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
            (select g_stream_claimed v_40656577200))
     true))
(assert (= (ora.field.value struct_init_40644503568)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644503568)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (ora.field.overflow struct_init_40644503568) true))
(assert (= (ora.field.value struct_init_40644504688)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644504688)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (bvugt (ora.field.value struct_init_40644504688)
            (select g_stream_deposit v_40656577200))
     true))
(assert (xor (bvult g_total_escrowed
            (bvsub (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                   (select g_stream_claimed v_40656577200)))
     true))
(assert (let ((a!1 (xor (bvult #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                       (bvsub (accruedAt_6129c65b415ce3b8_r0
                                v_40656577200
                                v_40656577296)
                              (select g_stream_claimed v_40656577200)))
                true)))
  (not a!1)))



Q6 - obligation


    

  • Function: claim
    • 

  • Location: loc("erc20_stream_core.ora":301:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577248 () (_ BitVec 160))
(declare-fun v_40656577200 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_recipient () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577296 () (_ BitVec 256))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644503568 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644504688 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_claimed () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577248 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577200) true true))
(assert (xor (not (= (select g_stream_recipient v_40656577200) v_40656577248)) true))
(assert (xor (bvule (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
            (select g_stream_claimed v_40656577200))
     true))
(assert (= (ora.field.value struct_init_40644503568)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644503568)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (ora.field.overflow struct_init_40644503568) true))
(assert (= (ora.field.value struct_init_40644504688)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644504688)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (bvugt (ora.field.value struct_init_40644504688)
            (select g_stream_deposit v_40656577200))
     true))
(assert (xor (bvult g_total_escrowed
            (bvsub (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                   (select g_stream_claimed v_40656577200)))
     true))
(assert (let ((a!1 (bvugt g_spec_total_claimed
                  (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                         (bvsub (accruedAt_6129c65b415ce3b8_r0
                                  v_40656577200
                                  v_40656577296)
                                (select g_stream_claimed v_40656577200))))))
  (xor a!1 true)))
(assert (let ((a!1 (bvsub (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                  (select (store g_stream_claimed
                                 v_40656577200
                                 (accruedAt_6129c65b415ce3b8_r0
                                   v_40656577200
                                   v_40656577296))
                          v_40656577200))))
  (not (xor (bvult g_total_escrowed a!1) true))))



Q7 - obligation


    

  • Function: claim
    • 

  • Location: loc("erc20_stream_core.ora":302:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577248 () (_ BitVec 160))
(declare-fun v_40656577200 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_recipient () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577296 () (_ BitVec 256))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644503568 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644504688 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_claimed () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577248 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577200) true true))
(assert (xor (not (= (select g_stream_recipient v_40656577200) v_40656577248)) true))
(assert (xor (bvule (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
            (select g_stream_claimed v_40656577200))
     true))
(assert (= (ora.field.value struct_init_40644503568)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644503568)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (ora.field.overflow struct_init_40644503568) true))
(assert (= (ora.field.value struct_init_40644504688)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644504688)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (bvugt (ora.field.value struct_init_40644504688)
            (select g_stream_deposit v_40656577200))
     true))
(assert (xor (bvult g_total_escrowed
            (bvsub (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                   (select g_stream_claimed v_40656577200)))
     true))
(assert (let ((a!1 (bvugt g_spec_total_claimed
                  (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                         (bvsub (accruedAt_6129c65b415ce3b8_r0
                                  v_40656577200
                                  v_40656577296)
                                (select g_stream_claimed v_40656577200))))))
  (xor a!1 true)))
(assert (let ((a!1 (bvsub (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                  (select (store g_stream_claimed
                                 v_40656577200
                                 (accruedAt_6129c65b415ce3b8_r0
                                   v_40656577200
                                   v_40656577296))
                          v_40656577200))))
  (not (xor (bvult (bvadd g_spec_total_claimed a!1) g_spec_total_claimed) true))))



Q8 - obligation


    

  • Function: claim
    • 

  • Location: loc("erc20_stream_core.ora":304:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577248 () (_ BitVec 160))
(declare-fun v_40656577200 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_recipient () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577296 () (_ BitVec 256))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644503568 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644504688 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_claimed () (_ BitVec 256))
(declare-fun struct_init_40644506768 () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577248 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577200) true true))
(assert (xor (not (= (select g_stream_recipient v_40656577200) v_40656577248)) true))
(assert (xor (bvule (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
            (select g_stream_claimed v_40656577200))
     true))
(assert (= (ora.field.value struct_init_40644503568)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644503568)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (ora.field.overflow struct_init_40644503568) true))
(assert (= (ora.field.value struct_init_40644504688)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644504688)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (bvugt (ora.field.value struct_init_40644504688)
            (select g_stream_deposit v_40656577200))
     true))
(assert (xor (bvult g_total_escrowed
            (bvsub (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                   (select g_stream_claimed v_40656577200)))
     true))
(assert (let ((a!1 (bvugt g_spec_total_claimed
                  (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                         (bvsub (accruedAt_6129c65b415ce3b8_r0
                                  v_40656577200
                                  v_40656577296)
                                (select g_stream_claimed v_40656577200))))))
  (xor a!1 true)))
(assert (let ((a!1 (bvadd (select (store g_stream_claimed
                                 v_40656577200
                                 (accruedAt_6129c65b415ce3b8_r0
                                   v_40656577200
                                   v_40656577296))
                          v_40656577200)
                  (select g_stream_reclaimed v_40656577200))))
  (= (ora.field.value struct_init_40644506768) a!1)))
(assert (let ((a!1 (bvadd (select (store g_stream_claimed
                                 v_40656577200
                                 (accruedAt_6129c65b415ce3b8_r0
                                   v_40656577200
                                   v_40656577296))
                          v_40656577200)
                  (select g_stream_reclaimed v_40656577200))))
(let ((a!2 (bvult a!1
                  (select (store g_stream_claimed
                                 v_40656577200
                                 (accruedAt_6129c65b415ce3b8_r0
                                   v_40656577200
                                   v_40656577296))
                          v_40656577200))))
  (= (ora.field.overflow struct_init_40644506768) a!2))))
(assert (not (xor (ora.field.overflow struct_init_40644506768) true)))



Q9 - obligation


    

  • Function: claim
    • 

  • Location: loc("erc20_stream_core.ora":305:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577248 () (_ BitVec 160))
(declare-fun v_40656577200 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_recipient () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577296 () (_ BitVec 256))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644503568 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644504688 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_claimed () (_ BitVec 256))
(declare-fun struct_init_40644507568 () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577248 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577200) true true))
(assert (xor (not (= (select g_stream_recipient v_40656577200) v_40656577248)) true))
(assert (xor (bvule (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
            (select g_stream_claimed v_40656577200))
     true))
(assert (= (ora.field.value struct_init_40644503568)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644503568)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (ora.field.overflow struct_init_40644503568) true))
(assert (= (ora.field.value struct_init_40644504688)
   (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
          (select g_stream_reclaimed v_40656577200))))
(assert (= (ora.field.overflow struct_init_40644504688)
   (bvult (bvadd (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                 (select g_stream_reclaimed v_40656577200))
          (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296))))
(assert (xor (bvugt (ora.field.value struct_init_40644504688)
            (select g_stream_deposit v_40656577200))
     true))
(assert (xor (bvult g_total_escrowed
            (bvsub (accruedAt_6129c65b415ce3b8_r0 v_40656577200 v_40656577296)
                   (select g_stream_claimed v_40656577200)))
     true))
(assert (let ((a!1 (bvugt g_spec_total_claimed
                  (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                         (bvsub (accruedAt_6129c65b415ce3b8_r0
                                  v_40656577200
                                  v_40656577296)
                                (select g_stream_claimed v_40656577200))))))
  (xor a!1 true)))
(assert (let ((a!1 (bvadd (select (store g_stream_claimed
                                 v_40656577200
                                 (accruedAt_6129c65b415ce3b8_r0
                                   v_40656577200
                                   v_40656577296))
                          v_40656577200)
                  (select g_stream_reclaimed v_40656577200))))
  (= (ora.field.value struct_init_40644507568) a!1)))
(assert (let ((a!1 (bvadd (select (store g_stream_claimed
                                 v_40656577200
                                 (accruedAt_6129c65b415ce3b8_r0
                                   v_40656577200
                                   v_40656577296))
                          v_40656577200)
                  (select g_stream_reclaimed v_40656577200))))
(let ((a!2 (bvult a!1
                  (select (store g_stream_claimed
                                 v_40656577200
                                 (accruedAt_6129c65b415ce3b8_r0
                                   v_40656577200
                                   v_40656577296))
                          v_40656577200))))
  (= (ora.field.overflow struct_init_40644507568) a!2))))
(assert (not (bvule (ora.field.value struct_init_40644507568)
            (select g_stream_deposit v_40656577200))))



Q10 - base


    

  • Function: assertLedgerInvariant
    • 

  • Location: loc("erc20_stream_core.ora":98:0
    • 

  • Status: SAT
    • 

  • Elapsed ms: 5
    • 

  • SMT-LIB:
    • 



(declare-fun g_spec_total_claimed () (_ BitVec 256))
(declare-fun g_spec_total_opened () (_ BitVec 256))
(declare-fun g_spec_total_reclaimed () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (bvuge g_spec_total_opened g_spec_total_claimed))
(assert (bvuge (bvsub g_spec_total_opened g_spec_total_claimed) g_spec_total_reclaimed))
(assert (= g_total_escrowed
   (bvsub (bvsub g_spec_total_opened g_spec_total_claimed)
          g_spec_total_reclaimed)))



Q11 - obligation


    

  • Function: assertLedgerInvariant
    • 

  • Location: loc("erc20_stream_core.ora":99:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun g_spec_total_claimed () (_ BitVec 256))
(declare-fun g_spec_total_opened () (_ BitVec 256))
(declare-fun g_spec_total_reclaimed () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (bvuge g_spec_total_opened g_spec_total_claimed))
(assert (bvuge (bvsub g_spec_total_opened g_spec_total_claimed) g_spec_total_reclaimed))
(assert (= g_total_escrowed
   (bvsub (bvsub g_spec_total_opened g_spec_total_claimed)
          g_spec_total_reclaimed)))
(assert (not (xor (bvult g_spec_total_opened g_spec_total_claimed) true)))



Q12 - obligation


    

  • Function: assertLedgerInvariant
    • 

  • Location: loc("erc20_stream_core.ora":100:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun g_spec_total_claimed () (_ BitVec 256))
(declare-fun g_spec_total_opened () (_ BitVec 256))
(declare-fun g_spec_total_reclaimed () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (bvuge g_spec_total_opened g_spec_total_claimed))
(assert (bvuge (bvsub g_spec_total_opened g_spec_total_claimed) g_spec_total_reclaimed))
(assert (= g_total_escrowed
   (bvsub (bvsub g_spec_total_opened g_spec_total_claimed)
          g_spec_total_reclaimed)))
(assert (not (xor (bvult g_spec_total_opened g_spec_total_claimed) true)))



Q13 - obligation


    

  • Function: assertLedgerInvariant
    • 

  • Location: loc("erc20_stream_core.ora":100:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun g_spec_total_claimed () (_ BitVec 256))
(declare-fun g_spec_total_opened () (_ BitVec 256))
(declare-fun g_spec_total_reclaimed () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (bvuge g_spec_total_opened g_spec_total_claimed))
(assert (bvuge (bvsub g_spec_total_opened g_spec_total_claimed) g_spec_total_reclaimed))
(assert (= g_total_escrowed
   (bvsub (bvsub g_spec_total_opened g_spec_total_claimed)
          g_spec_total_reclaimed)))
(assert (not (xor (bvult (bvsub g_spec_total_opened g_spec_total_claimed)
                 g_spec_total_reclaimed)
          true)))



Q14 - obligation


    

  • Function: assertLedgerInvariant
    • 

  • Location: loc("erc20_stream_core.ora":102:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun g_spec_total_claimed () (_ BitVec 256))
(declare-fun g_spec_total_opened () (_ BitVec 256))
(declare-fun g_spec_total_reclaimed () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (bvuge g_spec_total_opened g_spec_total_claimed))
(assert (bvuge (bvsub g_spec_total_opened g_spec_total_claimed) g_spec_total_reclaimed))
(assert (= g_total_escrowed
   (bvsub (bvsub g_spec_total_opened g_spec_total_claimed)
          g_spec_total_reclaimed)))
(assert (not (xor (bvult g_spec_total_opened g_spec_total_claimed) true)))



Q15 - obligation


    

  • Function: assertLedgerInvariant
    • 

  • Location: loc("erc20_stream_core.ora":103:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun g_spec_total_claimed () (_ BitVec 256))
(declare-fun g_spec_total_opened () (_ BitVec 256))
(declare-fun g_spec_total_reclaimed () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (bvuge g_spec_total_opened g_spec_total_claimed))
(assert (bvuge (bvsub g_spec_total_opened g_spec_total_claimed) g_spec_total_reclaimed))
(assert (= g_total_escrowed
   (bvsub (bvsub g_spec_total_opened g_spec_total_claimed)
          g_spec_total_reclaimed)))
(assert (not (xor (bvult (bvsub g_spec_total_opened g_spec_total_claimed)
                 g_spec_total_reclaimed)
          true)))



Q16 - obligation


    

  • Function: assertLedgerInvariant
    • 

  • Location: loc("erc20_stream_core.ora":104:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun g_spec_total_claimed () (_ BitVec 256))
(declare-fun g_spec_total_opened () (_ BitVec 256))
(declare-fun g_spec_total_reclaimed () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (bvuge g_spec_total_opened g_spec_total_claimed))
(assert (bvuge (bvsub g_spec_total_opened g_spec_total_claimed) g_spec_total_reclaimed))
(assert (= g_total_escrowed
   (bvsub (bvsub g_spec_total_opened g_spec_total_claimed)
          g_spec_total_reclaimed)))
(assert (not (= g_total_escrowed
        (bvsub (bvsub g_spec_total_opened g_spec_total_claimed)
               g_spec_total_reclaimed))))



Q17 - base


    

  • Function: closeStream
    • 

  • Location: loc("erc20_stream_core.ora":218:0
    • 

  • Status: SAT
    • 

  • Elapsed ms: 0
    • 

  • SMT-LIB:
    • 





Q18 - obligation


    

  • Function: closeStream
    • 

  • Location: loc("erc20_stream_core.ora":244:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576960 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_start () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_end () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577008 () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (select g_stream_exists v_40656576960) true true))
(assert (xor (select g_stream_open v_40656576960) true true))
(assert (xor (bvult (select g_stream_end v_40656576960)
            (select g_stream_start v_40656576960))
     true))
(assert (let ((a!1 (ite (bvult v_40656577008 (select g_stream_start v_40656576960))
                (select g_stream_start v_40656576960)
                v_40656577008)))
(let ((a!2 (accruedAt_6129c65b415ce3b8_r0
             v_40656576960
             (ite (bvugt a!1 (select g_stream_end v_40656576960))
                  (select g_stream_end v_40656576960)
                  a!1))))
  (xor (bvugt a!2 (select g_stream_deposit v_40656576960)) true))))
(assert (not (xor (select (store g_stream_open v_40656576960 false) v_40656576960) true)))



Q19 - obligation


    

  • Function: closeStream
    • 

  • Location: loc("erc20_stream_core.ora":245:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 77
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576960 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_start () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_end () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577008 () (_ BitVec 256))
(declare-fun g_stream_closed_at () (Array (_ BitVec 256) (_ BitVec 256)))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (select g_stream_exists v_40656576960) true true))
(assert (xor (select g_stream_open v_40656576960) true true))
(assert (xor (bvult (select g_stream_end v_40656576960)
            (select g_stream_start v_40656576960))
     true))
(assert (let ((a!1 (ite (bvult v_40656577008 (select g_stream_start v_40656576960))
                (select g_stream_start v_40656576960)
                v_40656577008)))
(let ((a!2 (accruedAt_6129c65b415ce3b8_r0
             v_40656576960
             (ite (bvugt a!1 (select g_stream_end v_40656576960))
                  (select g_stream_end v_40656576960)
                  a!1))))
  (xor (bvugt a!2 (select g_stream_deposit v_40656576960)) true))))
(assert (let ((a!1 (ite (bvult v_40656577008 (select g_stream_start v_40656576960))
                (select g_stream_start v_40656576960)
                v_40656577008)))
(let ((a!2 (store g_stream_closed_at
                  v_40656576960
                  (ite (bvugt a!1 (select g_stream_end v_40656576960))
                       (select g_stream_end v_40656576960)
                       a!1))))
  (not (bvuge (select a!2 v_40656576960) (select g_stream_start v_40656576960))))))



Q20 - obligation


    

  • Function: closeStream
    • 

  • Location: loc("erc20_stream_core.ora":246:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 58
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576960 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_start () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_end () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577008 () (_ BitVec 256))
(declare-fun g_stream_closed_at () (Array (_ BitVec 256) (_ BitVec 256)))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (select g_stream_exists v_40656576960) true true))
(assert (xor (select g_stream_open v_40656576960) true true))
(assert (xor (bvult (select g_stream_end v_40656576960)
            (select g_stream_start v_40656576960))
     true))
(assert (let ((a!1 (ite (bvult v_40656577008 (select g_stream_start v_40656576960))
                (select g_stream_start v_40656576960)
                v_40656577008)))
(let ((a!2 (accruedAt_6129c65b415ce3b8_r0
             v_40656576960
             (ite (bvugt a!1 (select g_stream_end v_40656576960))
                  (select g_stream_end v_40656576960)
                  a!1))))
  (xor (bvugt a!2 (select g_stream_deposit v_40656576960)) true))))
(assert (let ((a!1 (ite (bvult v_40656577008 (select g_stream_start v_40656576960))
                (select g_stream_start v_40656576960)
                v_40656577008)))
(let ((a!2 (store g_stream_closed_at
                  v_40656576960
                  (ite (bvugt a!1 (select g_stream_end v_40656576960))
                       (select g_stream_end v_40656576960)
                       a!1))))
  (not (bvule (select a!2 v_40656576960) (select g_stream_end v_40656576960))))))



Q21 - obligation


    

  • Function: closeStream
    • 

  • Location: loc("erc20_stream_core.ora":247:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576960 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_start () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_end () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577008 () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (select g_stream_exists v_40656576960) true true))
(assert (xor (select g_stream_open v_40656576960) true true))
(assert (xor (bvult (select g_stream_end v_40656576960)
            (select g_stream_start v_40656576960))
     true))
(assert (let ((a!1 (ite (bvult v_40656577008 (select g_stream_start v_40656576960))
                (select g_stream_start v_40656576960)
                v_40656577008)))
(let ((a!2 (accruedAt_6129c65b415ce3b8_r0
             v_40656576960
             (ite (bvugt a!1 (select g_stream_end v_40656576960))
                  (select g_stream_end v_40656576960)
                  a!1))))
  (xor (bvugt a!2 (select g_stream_deposit v_40656576960)) true))))
(assert (let ((a!1 (ite (bvult v_40656577008 (select g_stream_start v_40656576960))
                (select g_stream_start v_40656576960)
                v_40656577008)))
(let ((a!2 (accruedAt_6129c65b415ce3b8_r0
             v_40656576960
             (ite (bvugt a!1 (select g_stream_end v_40656576960))
                  (select g_stream_end v_40656576960)
                  a!1))))
  (not (bvule a!2 (select g_stream_deposit v_40656576960))))))



Q22 - base


    

  • Function: claimableNow
    • 

  • Location: loc("erc20_stream_core.ora":256:0
    • 

  • Status: SAT
    • 

  • Elapsed ms: 0
    • 

  • SMT-LIB:
    • 





Q23 - obligation


    

  • Function: claimableNow
    • 

  • Location: loc("erc20_stream_core.ora":262:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 17
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun v_40656577104 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577152 () (_ BitVec 256))
(assert (xor (select g_stream_exists v_40656577104) true true))
(assert (not (bvule (accruedAt_6129c65b415ce3b8_r0 v_40656577104 v_40656577152)
            (select g_stream_claimed v_40656577104))))
(assert (not (xor (bvult (accruedAt_6129c65b415ce3b8_r0 v_40656577104 v_40656577152)
                 (select g_stream_claimed v_40656577104))
          true)))



Q24 - base


    

  • Function: reclaim
    • 

  • Location: loc("erc20_stream_core.ora":337:0
    • 

  • Status: SAT
    • 

  • Elapsed ms: 0
    • 

  • SMT-LIB:
    • 





Q25 - obligation


    

  • Function: reclaim
    • 

  • Location: loc("erc20_stream_core.ora":354:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 17
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577488 () (_ BitVec 160))
(declare-fun v_40656577440 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_sender () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577536 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577488 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577440) true true))
(assert (xor (select g_stream_open v_40656577440) true))
(assert (xor (not (= (select g_stream_sender v_40656577440) v_40656577488)) true))
(assert (bvugt (select g_stream_deposit v_40656577440)
       (accruedAt_6129c65b415ce3b8_r0 v_40656577440 v_40656577536)))
(assert (bvugt (select g_stream_deposit v_40656577440)
       (accruedAt_6129c65b415ce3b8_r0 v_40656577440 v_40656577536)))
(assert (not (xor (bvult (select g_stream_deposit v_40656577440)
                 (accruedAt_6129c65b415ce3b8_r0 v_40656577440 v_40656577536))
          true)))



Q26 - obligation


    

  • Function: reclaim
    • 

  • Location: loc("erc20_stream_core.ora":367:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 87
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577488 () (_ BitVec 160))
(declare-fun v_40656577440 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_sender () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577536 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644583408 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644585008 () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577488 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577440) true true))
(assert (xor (select g_stream_open v_40656577440) true))
(assert (xor (not (= (select g_stream_sender v_40656577440) v_40656577488)) true))
(assert (let ((a!1 (bvule (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor a!1 true)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644583408) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644583408)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (ora.field.overflow struct_init_40644583408) true))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644585008) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644585008)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (bvugt (ora.field.value struct_init_40644585008)
            (select g_stream_deposit v_40656577440))
     true))
(assert (let ((a!1 (bvult (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (not (xor a!1 true))))



Q27 - obligation


    

  • Function: reclaim
    • 

  • Location: loc("erc20_stream_core.ora":371:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577488 () (_ BitVec 160))
(declare-fun v_40656577440 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_sender () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577536 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644583408 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644585008 () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577488 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577440) true true))
(assert (xor (select g_stream_open v_40656577440) true))
(assert (xor (not (= (select g_stream_sender v_40656577440) v_40656577488)) true))
(assert (let ((a!1 (bvule (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor a!1 true)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644583408) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644583408)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (ora.field.overflow struct_init_40644583408) true))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644585008) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644585008)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (bvugt (ora.field.value struct_init_40644585008)
            (select g_stream_deposit v_40656577440))
     true))
(assert (let ((a!1 (bvsub (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor (bvult g_total_escrowed a!1) true)))
(assert (let ((a!1 (bvsub (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (not (xor (bvult #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   a!1)
            true))))



Q28 - obligation


    

  • Function: reclaim
    • 

  • Location: loc("erc20_stream_core.ora":371:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577488 () (_ BitVec 160))
(declare-fun v_40656577440 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_sender () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577536 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644583408 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644585008 () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577488 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577440) true true))
(assert (xor (select g_stream_open v_40656577440) true))
(assert (xor (not (= (select g_stream_sender v_40656577440) v_40656577488)) true))
(assert (let ((a!1 (bvule (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor a!1 true)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644583408) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644583408)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (ora.field.overflow struct_init_40644583408) true))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644585008) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644585008)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (bvugt (ora.field.value struct_init_40644585008)
            (select g_stream_deposit v_40656577440))
     true))
(assert (let ((a!1 (bvsub (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor (bvult g_total_escrowed a!1) true)))
(assert (let ((a!1 (bvsub (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (not (xor (bvult #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   a!1)
            true))))



Q29 - obligation


    

  • Function: reclaim
    • 

  • Location: loc("erc20_stream_core.ora":371:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577488 () (_ BitVec 160))
(declare-fun v_40656577440 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_sender () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577536 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644583408 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644585008 () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577488 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577440) true true))
(assert (xor (select g_stream_open v_40656577440) true))
(assert (xor (not (= (select g_stream_sender v_40656577440) v_40656577488)) true))
(assert (let ((a!1 (bvule (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor a!1 true)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644583408) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644583408)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (ora.field.overflow struct_init_40644583408) true))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644585008) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644585008)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (bvugt (ora.field.value struct_init_40644585008)
            (select g_stream_deposit v_40656577440))
     true))
(assert (let ((a!1 (bvsub (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor (bvult g_total_escrowed a!1) true)))
(assert (let ((a!1 (bvsub (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (not (xor (bvult #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   a!1)
            true))))



Q30 - obligation


    

  • Function: reclaim
    • 

  • Location: loc("erc20_stream_core.ora":375:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577488 () (_ BitVec 160))
(declare-fun v_40656577440 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_sender () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577536 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644583408 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644585008 () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_reclaimed () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577488 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577440) true true))
(assert (xor (select g_stream_open v_40656577440) true))
(assert (xor (not (= (select g_stream_sender v_40656577440) v_40656577488)) true))
(assert (let ((a!1 (bvule (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor a!1 true)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644583408) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644583408)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (ora.field.overflow struct_init_40644583408) true))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644585008) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644585008)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (bvugt (ora.field.value struct_init_40644585008)
            (select g_stream_deposit v_40656577440))
     true))
(assert (let ((a!1 (bvsub (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor (bvult g_total_escrowed a!1) true)))
(assert (let ((a!1 (bvsub (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor (bvugt g_spec_total_reclaimed
              (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                     a!1))
       true)))
(assert (let ((a!1 (ite (bvugt (select g_stream_deposit v_40656577440)
                       (accruedAt_6129c65b415ce3b8_r0
                         v_40656577440
                         v_40656577536))
                (bvsub (select g_stream_deposit v_40656577440)
                       (accruedAt_6129c65b415ce3b8_r0
                         v_40656577440
                         v_40656577536))
                #x0000000000000000000000000000000000000000000000000000000000000000)))
(let ((a!2 (bvult g_total_escrowed
                  (bvsub a!1
                         (select (store g_stream_reclaimed v_40656577440 a!1)
                                 v_40656577440)))))
  (not (xor a!2 true)))))



Q31 - obligation


    

  • Function: reclaim
    • 

  • Location: loc("erc20_stream_core.ora":376:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577488 () (_ BitVec 160))
(declare-fun v_40656577440 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_sender () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577536 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644583408 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644585008 () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_reclaimed () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577488 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577440) true true))
(assert (xor (select g_stream_open v_40656577440) true))
(assert (xor (not (= (select g_stream_sender v_40656577440) v_40656577488)) true))
(assert (let ((a!1 (bvule (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor a!1 true)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644583408) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644583408)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (ora.field.overflow struct_init_40644583408) true))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644585008) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644585008)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (bvugt (ora.field.value struct_init_40644585008)
            (select g_stream_deposit v_40656577440))
     true))
(assert (let ((a!1 (bvsub (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor (bvult g_total_escrowed a!1) true)))
(assert (let ((a!1 (bvsub (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor (bvugt g_spec_total_reclaimed
              (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                     a!1))
       true)))
(assert (let ((a!1 (ite (bvugt (select g_stream_deposit v_40656577440)
                       (accruedAt_6129c65b415ce3b8_r0
                         v_40656577440
                         v_40656577536))
                (bvsub (select g_stream_deposit v_40656577440)
                       (accruedAt_6129c65b415ce3b8_r0
                         v_40656577440
                         v_40656577536))
                #x0000000000000000000000000000000000000000000000000000000000000000)))
(let ((a!2 (bvadd g_spec_total_reclaimed
                  (bvsub a!1
                         (select (store g_stream_reclaimed v_40656577440 a!1)
                                 v_40656577440)))))
  (not (xor (bvult a!2 g_spec_total_reclaimed) true)))))



Q32 - obligation


    

  • Function: reclaim
    • 

  • Location: loc("erc20_stream_core.ora":378:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577488 () (_ BitVec 160))
(declare-fun v_40656577440 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_sender () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577536 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644583408 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644585008 () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_reclaimed () (_ BitVec 256))
(declare-fun struct_init_40644587408 () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577488 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577440) true true))
(assert (xor (select g_stream_open v_40656577440) true))
(assert (xor (not (= (select g_stream_sender v_40656577440) v_40656577488)) true))
(assert (let ((a!1 (bvule (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor a!1 true)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644583408) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644583408)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (ora.field.overflow struct_init_40644583408) true))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644585008) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644585008)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (bvugt (ora.field.value struct_init_40644585008)
            (select g_stream_deposit v_40656577440))
     true))
(assert (let ((a!1 (bvsub (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor (bvult g_total_escrowed a!1) true)))
(assert (let ((a!1 (bvsub (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor (bvugt g_spec_total_reclaimed
              (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                     a!1))
       true)))
(assert (let ((a!1 (store g_stream_reclaimed
                  v_40656577440
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644587408)
     (bvadd (select g_stream_claimed v_40656577440) (select a!1 v_40656577440)))))
(assert (let ((a!1 (store g_stream_reclaimed
                  v_40656577440
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644587408)
     (bvult (bvadd (select g_stream_claimed v_40656577440)
                   (select a!1 v_40656577440))
            (select g_stream_claimed v_40656577440)))))
(assert (not (xor (ora.field.overflow struct_init_40644587408) true)))



Q33 - obligation


    

  • Function: reclaim
    • 

  • Location: loc("erc20_stream_core.ora":379:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656577488 () (_ BitVec 160))
(declare-fun v_40656577440 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_sender () (Array (_ BitVec 256) (_ BitVec 160)))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577536 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun struct_init_40644583408 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644585008 () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_reclaimed () (_ BitVec 256))
(declare-fun struct_init_40644588208 () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656577488 #x0000000000000000000000000000000000000000) true))
(assert (xor (select g_stream_exists v_40656577440) true true))
(assert (xor (select g_stream_open v_40656577440) true))
(assert (xor (not (= (select g_stream_sender v_40656577440) v_40656577488)) true))
(assert (let ((a!1 (bvule (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor a!1 true)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644583408) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644583408)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (ora.field.overflow struct_init_40644583408) true))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644585008) a!1)))
(assert (let ((a!1 (bvadd (select g_stream_claimed v_40656577440)
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644585008)
     (bvult a!1 (select g_stream_claimed v_40656577440)))))
(assert (xor (bvugt (ora.field.value struct_init_40644585008)
            (select g_stream_deposit v_40656577440))
     true))
(assert (let ((a!1 (bvsub (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor (bvult g_total_escrowed a!1) true)))
(assert (let ((a!1 (bvsub (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577440))))
  (xor (bvugt g_spec_total_reclaimed
              (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                     a!1))
       true)))
(assert (let ((a!1 (store g_stream_reclaimed
                  v_40656577440
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.value struct_init_40644588208)
     (bvadd (select g_stream_claimed v_40656577440) (select a!1 v_40656577440)))))
(assert (let ((a!1 (store g_stream_reclaimed
                  v_40656577440
                  (ite (bvugt (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       (bvsub (select g_stream_deposit v_40656577440)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577440
                                v_40656577536))
                       #x0000000000000000000000000000000000000000000000000000000000000000))))
  (= (ora.field.overflow struct_init_40644588208)
     (bvult (bvadd (select g_stream_claimed v_40656577440)
                   (select a!1 v_40656577440))
            (select g_stream_claimed v_40656577440)))))
(assert (not (bvule (ora.field.value struct_init_40644588208)
            (select g_stream_deposit v_40656577440))))



Q34 - base


    

  • Function: refundableNow
    • 

  • Location: loc("erc20_stream_core.ora":315:0
    • 

  • Status: SAT
    • 

  • Elapsed ms: 0
    • 

  • SMT-LIB:
    • 





Q35 - obligation


    

  • Function: refundableNow
    • 

  • Location: loc("erc20_stream_core.ora":323:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 18
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun v_40656577344 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577392 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(assert (xor (select g_stream_exists v_40656577344) true true))
(assert (xor (select g_stream_open v_40656577344) true))
(assert (bvugt (select g_stream_deposit v_40656577344)
       (accruedAt_6129c65b415ce3b8_r0 v_40656577344 v_40656577392)))
(assert (bvugt (select g_stream_deposit v_40656577344)
       (accruedAt_6129c65b415ce3b8_r0 v_40656577344 v_40656577392)))
(assert (not (xor (bvult (select g_stream_deposit v_40656577344)
                 (accruedAt_6129c65b415ce3b8_r0 v_40656577344 v_40656577392))
          true)))



Q36 - obligation


    

  • Function: refundableNow
    • 

  • Location: loc("erc20_stream_core.ora":329:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 53
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun v_40656577344 () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun accruedAt_6129c65b415ce3b8_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(declare-fun v_40656577392 () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(assert (xor (select g_stream_exists v_40656577344) true true))
(assert (xor (select g_stream_open v_40656577344) true))
(assert (let ((a!1 (bvule (ite (bvugt (select g_stream_deposit v_40656577344)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577344
                                v_40656577392))
                       (bvsub (select g_stream_deposit v_40656577344)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577344
                                v_40656577392))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577344))))
  (not a!1)))
(assert (let ((a!1 (bvult (ite (bvugt (select g_stream_deposit v_40656577344)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577344
                                v_40656577392))
                       (bvsub (select g_stream_deposit v_40656577344)
                              (accruedAt_6129c65b415ce3b8_r0
                                v_40656577344
                                v_40656577392))
                       #x0000000000000000000000000000000000000000000000000000000000000000)
                  (select g_stream_reclaimed v_40656577344))))
  (not (xor a!1 true))))



Q37 - base


    

  • Function: init
    • 

  • Location: loc("erc20_stream_core.ora":65:0
    • 

  • Status: SAT
    • 

  • Elapsed ms: 0
    • 

  • SMT-LIB:
    • 



(declare-fun v_40656575088 () (_ BitVec 160))
(declare-fun v_40656575136 () (_ BitVec 160))
(assert (not (= v_40656575088 #x0000000000000000000000000000000000000000)))
(assert (not (= v_40656575136 #x0000000000000000000000000000000000000000)))



Q38 - guard_satisfy


    

  • Function: init
    • 

  • Location: loc("erc20_stream_core.ora":65:0
    • 

  • Status: SAT
    • 

  • Elapsed ms: 0
    • 

  • Guard ID: guard:erc20_stream_core.ora:65:17:5:non_zero_address:token
    • 

  • SMT-LIB:
    • 



(declare-fun v_40656575088 () (_ BitVec 160))
(declare-fun v_40656575136 () (_ BitVec 160))
(assert (not (= v_40656575088 #x0000000000000000000000000000000000000000)))
(assert (not (= v_40656575136 #x0000000000000000000000000000000000000000)))
(assert (not (= ((_ extract 159 0) v_40656575088)
        #x0000000000000000000000000000000000000000)))



Q39 - guard_violate


    

  • Function: init
    • 

  • Location: loc("erc20_stream_core.ora":65:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Guard ID: guard:erc20_stream_core.ora:65:17:5:non_zero_address:token
    • 

  • SMT-LIB:
    • 



(declare-fun v_40656575088 () (_ BitVec 160))
(declare-fun v_40656575136 () (_ BitVec 160))
(assert (not (= v_40656575088 #x0000000000000000000000000000000000000000)))
(assert (not (= v_40656575136 #x0000000000000000000000000000000000000000)))
(assert (not (not (= ((_ extract 159 0) v_40656575088)
             #x0000000000000000000000000000000000000000))))



Q40 - guard_satisfy


    

  • Function: init
    • 

  • Location: loc("erc20_stream_core.ora":65:0
    • 

  • Status: SAT
    • 

  • Elapsed ms: 0
    • 

  • Guard ID: guard:erc20_stream_core.ora:65:40:7:non_zero_address:adapter
    • 

  • SMT-LIB:
    • 



(declare-fun v_40656575088 () (_ BitVec 160))
(declare-fun v_40656575136 () (_ BitVec 160))
(assert (not (= v_40656575088 #x0000000000000000000000000000000000000000)))
(assert (not (= v_40656575136 #x0000000000000000000000000000000000000000)))
(assert (not (= ((_ extract 159 0) v_40656575088)
        #x0000000000000000000000000000000000000000)))
(assert (not (= ((_ extract 159 0) v_40656575136)
        #x0000000000000000000000000000000000000000)))



Q41 - guard_violate


    

  • Function: init
    • 

  • Location: loc("erc20_stream_core.ora":65:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Guard ID: guard:erc20_stream_core.ora:65:40:7:non_zero_address:adapter
    • 

  • SMT-LIB:
    • 



(declare-fun v_40656575088 () (_ BitVec 160))
(declare-fun v_40656575136 () (_ BitVec 160))
(assert (not (= v_40656575088 #x0000000000000000000000000000000000000000)))
(assert (not (= v_40656575136 #x0000000000000000000000000000000000000000)))
(assert (not (= ((_ extract 159 0) v_40656575088)
        #x0000000000000000000000000000000000000000)))
(assert (not (not (= ((_ extract 159 0) v_40656575136)
             #x0000000000000000000000000000000000000000))))



Q42 - base


    

  • Function: accruedAt
    • 

  • Location: loc("erc20_stream_core.ora":124:0
    • 

  • Status: SAT
    • 

  • Elapsed ms: 0
    • 

  • SMT-LIB:
    • 





Q43 - obligation


    

  • Function: accruedAt
    • 

  • Location: loc("erc20_stream_core.ora":128:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 21
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun v_40656576144 () (_ BitVec 256))
(declare-fun g_stream_start () (Array (_ BitVec 256) (_ BitVec 256)))
(declare-fun v_40656576192 () (_ BitVec 256))
(declare-fun streamCutoff_af060e52937e903c_r0
             ((_ BitVec 256) (_ BitVec 256))
             (_ BitVec 256))
(assert (xor (bvule v_40656576192 (select g_stream_start v_40656576144)) true))
(assert (bvugt (streamCutoff_af060e52937e903c_r0 v_40656576144 v_40656576192)
       (select g_stream_start v_40656576144)))
(assert (not (xor (bvult (streamCutoff_af060e52937e903c_r0 v_40656576144 v_40656576192)
                 (select g_stream_start v_40656576144))
          true)))



Q44 - base


    

  • Function: streamCutoff
    • 

  • Location: loc("erc20_stream_core.ora":113:0
    • 

  • Status: SAT
    • 

  • Elapsed ms: 0
    • 

  • SMT-LIB:
    • 





Q45 - base


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":150:0
    • 

  • Status: SAT
    • 

  • Elapsed ms: 0
    • 

  • SMT-LIB:
    • 





Q46 - obligation


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":168:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 23
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576576 () (_ BitVec 160))
(declare-fun v_40656576624 () (_ BitVec 160))
(declare-fun v_40656576768 () (_ BitVec 256))
(declare-fun v_40656576816 () (_ BitVec 256))
(declare-fun v_40656576672 () (_ BitVec 256))
(declare-fun v_40656576720 () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656576576 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576624 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576576 v_40656576624) true))
(assert (xor (= v_40656576768
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (xor (= v_40656576816
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (bvugt v_40656576720 v_40656576672))
(assert (not (xor (bvult v_40656576720 v_40656576672) true)))



Q47 - obligation


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":182:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576576 () (_ BitVec 160))
(declare-fun v_40656576624 () (_ BitVec 160))
(declare-fun v_40656576768 () (_ BitVec 256))
(declare-fun v_40656576816 () (_ BitVec 256))
(declare-fun v_40656576672 () (_ BitVec 256))
(declare-fun v_40656576720 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644339568 () (_ BitVec 256))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun g_next_stream_id () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656576576 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576624 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576576 v_40656576624) true))
(assert (xor (= v_40656576768
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (xor (= v_40656576816
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (bvugt v_40656576720 v_40656576672))
(assert (bvugt v_40656576720 v_40656576672))
(assert (xor (ora.field.overflow struct_init_40644339568) true))
(assert (xor (not (= (ora.field.value struct_init_40644339568) v_40656576816)) true))
(assert (xor (= g_next_stream_id
        #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
     true))
(assert (not (xor (bvult #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                 v_40656576816)
          true)))



Q48 - obligation


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":182:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576576 () (_ BitVec 160))
(declare-fun v_40656576624 () (_ BitVec 160))
(declare-fun v_40656576768 () (_ BitVec 256))
(declare-fun v_40656576816 () (_ BitVec 256))
(declare-fun v_40656576672 () (_ BitVec 256))
(declare-fun v_40656576720 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644339568 () (_ BitVec 256))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun g_next_stream_id () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656576576 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576624 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576576 v_40656576624) true))
(assert (xor (= v_40656576768
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (xor (= v_40656576816
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (bvugt v_40656576720 v_40656576672))
(assert (bvugt v_40656576720 v_40656576672))
(assert (xor (ora.field.overflow struct_init_40644339568) true))
(assert (xor (not (= (ora.field.value struct_init_40644339568) v_40656576816)) true))
(assert (xor (= g_next_stream_id
        #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
     true))
(assert (not (xor (bvult #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                 v_40656576816)
          true)))



Q49 - obligation


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":182:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576576 () (_ BitVec 160))
(declare-fun v_40656576624 () (_ BitVec 160))
(declare-fun v_40656576768 () (_ BitVec 256))
(declare-fun v_40656576816 () (_ BitVec 256))
(declare-fun v_40656576672 () (_ BitVec 256))
(declare-fun v_40656576720 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644339568 () (_ BitVec 256))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun g_next_stream_id () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656576576 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576624 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576576 v_40656576624) true))
(assert (xor (= v_40656576768
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (xor (= v_40656576816
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (bvugt v_40656576720 v_40656576672))
(assert (bvugt v_40656576720 v_40656576672))
(assert (xor (ora.field.overflow struct_init_40644339568) true))
(assert (xor (not (= (ora.field.value struct_init_40644339568) v_40656576816)) true))
(assert (xor (= g_next_stream_id
        #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
     true))
(assert (not (xor (bvult #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                 v_40656576816)
          true)))



Q50 - obligation


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":185:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576576 () (_ BitVec 160))
(declare-fun v_40656576624 () (_ BitVec 160))
(declare-fun v_40656576768 () (_ BitVec 256))
(declare-fun v_40656576816 () (_ BitVec 256))
(declare-fun v_40656576672 () (_ BitVec 256))
(declare-fun v_40656576720 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644339568 () (_ BitVec 256))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun g_next_stream_id () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656576576 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576624 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576576 v_40656576624) true))
(assert (xor (= v_40656576768
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (xor (= v_40656576816
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (bvugt v_40656576720 v_40656576672))
(assert (bvugt v_40656576720 v_40656576672))
(assert (xor (ora.field.overflow struct_init_40644339568) true))
(assert (xor (not (= (ora.field.value struct_init_40644339568) v_40656576816)) true))
(assert (xor (= g_next_stream_id
        #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
     true))
(assert (xor (bvugt g_total_escrowed
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (not (xor (bvult #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                 v_40656576816)
          true)))



Q51 - obligation


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":185:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576576 () (_ BitVec 160))
(declare-fun v_40656576624 () (_ BitVec 160))
(declare-fun v_40656576768 () (_ BitVec 256))
(declare-fun v_40656576816 () (_ BitVec 256))
(declare-fun v_40656576672 () (_ BitVec 256))
(declare-fun v_40656576720 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644339568 () (_ BitVec 256))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun g_next_stream_id () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656576576 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576624 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576576 v_40656576624) true))
(assert (xor (= v_40656576768
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (xor (= v_40656576816
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (bvugt v_40656576720 v_40656576672))
(assert (bvugt v_40656576720 v_40656576672))
(assert (xor (ora.field.overflow struct_init_40644339568) true))
(assert (xor (not (= (ora.field.value struct_init_40644339568) v_40656576816)) true))
(assert (xor (= g_next_stream_id
        #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
     true))
(assert (xor (bvugt g_total_escrowed
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (not (xor (bvult #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                 v_40656576816)
          true)))



Q52 - obligation


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":185:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576576 () (_ BitVec 160))
(declare-fun v_40656576624 () (_ BitVec 160))
(declare-fun v_40656576768 () (_ BitVec 256))
(declare-fun v_40656576816 () (_ BitVec 256))
(declare-fun v_40656576672 () (_ BitVec 256))
(declare-fun v_40656576720 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644339568 () (_ BitVec 256))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun g_next_stream_id () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656576576 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576624 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576576 v_40656576624) true))
(assert (xor (= v_40656576768
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (xor (= v_40656576816
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (bvugt v_40656576720 v_40656576672))
(assert (bvugt v_40656576720 v_40656576672))
(assert (xor (ora.field.overflow struct_init_40644339568) true))
(assert (xor (not (= (ora.field.value struct_init_40644339568) v_40656576816)) true))
(assert (xor (= g_next_stream_id
        #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
     true))
(assert (xor (bvugt g_total_escrowed
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (not (xor (bvult #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                 v_40656576816)
          true)))



Q53 - obligation


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":189:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 14
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576576 () (_ BitVec 160))
(declare-fun v_40656576624 () (_ BitVec 160))
(declare-fun v_40656576768 () (_ BitVec 256))
(declare-fun v_40656576816 () (_ BitVec 256))
(declare-fun v_40656576672 () (_ BitVec 256))
(declare-fun v_40656576720 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644339568 () (_ BitVec 256))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun g_next_stream_id () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_opened () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656576576 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576624 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576576 v_40656576624) true))
(assert (xor (= v_40656576768
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (xor (= v_40656576816
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (bvugt v_40656576720 v_40656576672))
(assert (bvugt v_40656576720 v_40656576672))
(assert (xor (ora.field.overflow struct_init_40644339568) true))
(assert (xor (not (= (ora.field.value struct_init_40644339568) v_40656576816)) true))
(assert (xor (= g_next_stream_id
        #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
     true))
(assert (xor (bvugt g_total_escrowed
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (xor (bvugt g_spec_total_opened
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (not (xor (bvult (bvadd g_next_stream_id
                        #x0000000000000000000000000000000000000000000000000000000000000001)
                 g_next_stream_id)
          true)))



Q54 - obligation


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":201:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 101
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576576 () (_ BitVec 160))
(declare-fun v_40656576624 () (_ BitVec 160))
(declare-fun v_40656576768 () (_ BitVec 256))
(declare-fun v_40656576816 () (_ BitVec 256))
(declare-fun v_40656576672 () (_ BitVec 256))
(declare-fun v_40656576720 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644339568 () (_ BitVec 256))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun g_next_stream_id () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_opened () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656576576 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576624 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576576 v_40656576624) true))
(assert (xor (= v_40656576768
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (xor (= v_40656576816
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (bvugt v_40656576720 v_40656576672))
(assert (bvugt v_40656576720 v_40656576672))
(assert (xor (ora.field.overflow struct_init_40644339568) true))
(assert (xor (not (= (ora.field.value struct_init_40644339568) v_40656576816)) true))
(assert (xor (= g_next_stream_id
        #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
     true))
(assert (xor (bvugt g_total_escrowed
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (xor (bvugt g_spec_total_opened
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (not (xor (bvult (bvadd g_total_escrowed v_40656576816) g_total_escrowed) true)))



Q55 - obligation


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":202:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 81
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576576 () (_ BitVec 160))
(declare-fun v_40656576624 () (_ BitVec 160))
(declare-fun v_40656576768 () (_ BitVec 256))
(declare-fun v_40656576816 () (_ BitVec 256))
(declare-fun v_40656576672 () (_ BitVec 256))
(declare-fun v_40656576720 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644339568 () (_ BitVec 256))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun g_next_stream_id () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_opened () (_ BitVec 256))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656576576 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576624 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576576 v_40656576624) true))
(assert (xor (= v_40656576768
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (xor (= v_40656576816
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (bvugt v_40656576720 v_40656576672))
(assert (bvugt v_40656576720 v_40656576672))
(assert (xor (ora.field.overflow struct_init_40644339568) true))
(assert (xor (not (= (ora.field.value struct_init_40644339568) v_40656576816)) true))
(assert (xor (= g_next_stream_id
        #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
     true))
(assert (xor (bvugt g_total_escrowed
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (xor (bvugt g_spec_total_opened
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (not (xor (bvult (bvadd g_spec_total_opened v_40656576816) g_spec_total_opened)
          true)))



Q56 - obligation


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":204:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576576 () (_ BitVec 160))
(declare-fun v_40656576624 () (_ BitVec 160))
(declare-fun v_40656576768 () (_ BitVec 256))
(declare-fun v_40656576816 () (_ BitVec 256))
(declare-fun v_40656576672 () (_ BitVec 256))
(declare-fun v_40656576720 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644339568 () (_ BitVec 256))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun g_next_stream_id () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_opened () (_ BitVec 256))
(declare-fun g_stream_exists () (Array (_ BitVec 256) Bool))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656576576 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576624 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576576 v_40656576624) true))
(assert (xor (= v_40656576768
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (xor (= v_40656576816
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (bvugt v_40656576720 v_40656576672))
(assert (bvugt v_40656576720 v_40656576672))
(assert (xor (ora.field.overflow struct_init_40644339568) true))
(assert (xor (not (= (ora.field.value struct_init_40644339568) v_40656576816)) true))
(assert (xor (= g_next_stream_id
        #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
     true))
(assert (xor (bvugt g_total_escrowed
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (xor (bvugt g_spec_total_opened
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (not (select (store g_stream_exists
                    (bvadd g_next_stream_id
                           #x0000000000000000000000000000000000000000000000000000000000000001)
                    true)
             (bvadd g_next_stream_id
                    #x0000000000000000000000000000000000000000000000000000000000000001))))



Q57 - obligation


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":205:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576576 () (_ BitVec 160))
(declare-fun v_40656576624 () (_ BitVec 160))
(declare-fun v_40656576768 () (_ BitVec 256))
(declare-fun v_40656576816 () (_ BitVec 256))
(declare-fun v_40656576672 () (_ BitVec 256))
(declare-fun v_40656576720 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644339568 () (_ BitVec 256))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun g_next_stream_id () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_opened () (_ BitVec 256))
(declare-fun g_stream_open () (Array (_ BitVec 256) Bool))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656576576 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576624 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576576 v_40656576624) true))
(assert (xor (= v_40656576768
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (xor (= v_40656576816
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (bvugt v_40656576720 v_40656576672))
(assert (bvugt v_40656576720 v_40656576672))
(assert (xor (ora.field.overflow struct_init_40644339568) true))
(assert (xor (not (= (ora.field.value struct_init_40644339568) v_40656576816)) true))
(assert (xor (= g_next_stream_id
        #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
     true))
(assert (xor (bvugt g_total_escrowed
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (xor (bvugt g_spec_total_opened
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (not (select (store g_stream_open
                    (bvadd g_next_stream_id
                           #x0000000000000000000000000000000000000000000000000000000000000001)
                    true)
             (bvadd g_next_stream_id
                    #x0000000000000000000000000000000000000000000000000000000000000001))))



Q58 - obligation


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":206:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576576 () (_ BitVec 160))
(declare-fun v_40656576624 () (_ BitVec 160))
(declare-fun v_40656576768 () (_ BitVec 256))
(declare-fun v_40656576816 () (_ BitVec 256))
(declare-fun v_40656576672 () (_ BitVec 256))
(declare-fun v_40656576720 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644339568 () (_ BitVec 256))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun g_next_stream_id () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_opened () (_ BitVec 256))
(declare-fun g_stream_claimed () (Array (_ BitVec 256) (_ BitVec 256)))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656576576 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576624 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576576 v_40656576624) true))
(assert (xor (= v_40656576768
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (xor (= v_40656576816
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (bvugt v_40656576720 v_40656576672))
(assert (bvugt v_40656576720 v_40656576672))
(assert (xor (ora.field.overflow struct_init_40644339568) true))
(assert (xor (not (= (ora.field.value struct_init_40644339568) v_40656576816)) true))
(assert (xor (= g_next_stream_id
        #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
     true))
(assert (xor (bvugt g_total_escrowed
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (xor (bvugt g_spec_total_opened
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (let ((a!1 (= (select (store g_stream_claimed
                             (bvadd g_next_stream_id
                                    #x0000000000000000000000000000000000000000000000000000000000000001)
                             #x0000000000000000000000000000000000000000000000000000000000000000)
                      (bvadd g_next_stream_id
                             #x0000000000000000000000000000000000000000000000000000000000000001))
              #x0000000000000000000000000000000000000000000000000000000000000000)))
  (not a!1)))



Q59 - obligation


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":207:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576576 () (_ BitVec 160))
(declare-fun v_40656576624 () (_ BitVec 160))
(declare-fun v_40656576768 () (_ BitVec 256))
(declare-fun v_40656576816 () (_ BitVec 256))
(declare-fun v_40656576672 () (_ BitVec 256))
(declare-fun v_40656576720 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644339568 () (_ BitVec 256))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun g_next_stream_id () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_opened () (_ BitVec 256))
(declare-fun g_stream_reclaimed () (Array (_ BitVec 256) (_ BitVec 256)))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656576576 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576624 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576576 v_40656576624) true))
(assert (xor (= v_40656576768
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (xor (= v_40656576816
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (bvugt v_40656576720 v_40656576672))
(assert (bvugt v_40656576720 v_40656576672))
(assert (xor (ora.field.overflow struct_init_40644339568) true))
(assert (xor (not (= (ora.field.value struct_init_40644339568) v_40656576816)) true))
(assert (xor (= g_next_stream_id
        #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
     true))
(assert (xor (bvugt g_total_escrowed
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (xor (bvugt g_spec_total_opened
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (let ((a!1 (= (select (store g_stream_reclaimed
                             (bvadd g_next_stream_id
                                    #x0000000000000000000000000000000000000000000000000000000000000001)
                             #x0000000000000000000000000000000000000000000000000000000000000000)
                      (bvadd g_next_stream_id
                             #x0000000000000000000000000000000000000000000000000000000000000001))
              #x0000000000000000000000000000000000000000000000000000000000000000)))
  (not a!1)))



Q60 - obligation


    

  • Function: openStream
    • 

  • Location: loc("erc20_stream_core.ora":208:0
    • 

  • Status: UNSAT
    • 

  • Elapsed ms: 0
    • 

  • Obligation kind: contract invariant
    • 

  • SMT-LIB:
    • 



(declare-fun onlyAdapter_ae632dd3975a0740_r0 () Bool)
(declare-fun v_40656576576 () (_ BitVec 160))
(declare-fun v_40656576624 () (_ BitVec 160))
(declare-fun v_40656576768 () (_ BitVec 256))
(declare-fun v_40656576816 () (_ BitVec 256))
(declare-fun v_40656576672 () (_ BitVec 256))
(declare-fun v_40656576720 () (_ BitVec 256))
(declare-fun ora.field.overflow ((_ BitVec 256)) Bool)
(declare-fun struct_init_40644339568 () (_ BitVec 256))
(declare-fun ora.field.value ((_ BitVec 256)) (_ BitVec 256))
(declare-fun g_next_stream_id () (_ BitVec 256))
(declare-fun g_total_escrowed () (_ BitVec 256))
(declare-fun g_spec_total_opened () (_ BitVec 256))
(declare-fun g_stream_deposit () (Array (_ BitVec 256) (_ BitVec 256)))
(assert (xor onlyAdapter_ae632dd3975a0740_r0 true true))
(assert (xor (= v_40656576576 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576624 #x0000000000000000000000000000000000000000) true))
(assert (xor (= v_40656576576 v_40656576624) true))
(assert (xor (= v_40656576768
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (xor (= v_40656576816
        #x0000000000000000000000000000000000000000000000000000000000000000)
     true))
(assert (bvugt v_40656576720 v_40656576672))
(assert (bvugt v_40656576720 v_40656576672))
(assert (xor (ora.field.overflow struct_init_40644339568) true))
(assert (xor (not (= (ora.field.value struct_init_40644339568) v_40656576816)) true))
(assert (xor (= g_next_stream_id
        #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)
     true))
(assert (xor (bvugt g_total_escrowed
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (xor (bvugt g_spec_total_opened
            (bvsub #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff
                   v_40656576816))
     true))
(assert (let ((a!1 (= (select (store g_stream_deposit
                             (bvadd g_next_stream_id
                                    #x0000000000000000000000000000000000000000000000000000000000000001)
                             v_40656576816)
                      (bvadd g_next_stream_id
                             #x0000000000000000000000000000000000000000000000000000000000000001))
              v_40656576816)))
  (not a!1)))




  


  






        
        

          

            

              









            


            

              

  
    Sign up for free
    to join this conversation on GitHub.
    Already have an account?
    Sign in to comment