counterexample.txt

=================== Baseline =============

      function f(x) {
    1    if (x)
    2      print("hi")
    3    call g()
    4    return
       }
    
       function g() {
    1    return
       }


================= Copy with framestate insertion =============

       function f'(x) {
    1    framestate f.1
    2    if (x)
    3      print("hi")
    4    call g()
    5    return
       }
    
       function g'() {
    1    framestate g.1
    2    return
       }

================ Speculate ===================================

       function f'(x) {
    1    framestate f.1
    2    assume !x, f.1
    3    call g()
    4    return
       }
    
       function g'() {
    1    framestate g.1
    2    return
       }

================ Hoist ===================================

## the callee g does not change x

       function f'(x) {
    1    framestate f.1
    2    call g()
    3    assume !x, f.1
    4    return
       }
    
       function g'() {
    1    framestate g.1
    2    return
       }



============= Inline (using framestate before the call) =============


       function f'(x) {
    1    framestate f.1
    2    framestate g.1, f.1+1     # <- now this framestate includes the assumption !x, but is not guarded by it...
    3    assume !x, f.1
    4    return
       }