============ initial translation from Move ================

[variant baseline]
fun Test::get_and_incr($t0|addr: address): u64 {
     var $t1|r: &mut Test::R
     var $t2|v: u64
     var $t3: address
     var $t4: bool
     var $t5: bool
     var $t6: u64
     var $t7: address
     var $t8: &mut Test::R
     var $t9: &mut Test::R
     var $t10: &u64
     var $t11: u64
     var $t12: &mut Test::R
     var $t13: &u64
     var $t14: u64
     var $t15: u64
     var $t16: u64
     var $t17: &mut Test::R
     var $t18: &mut u64
     var $t19: u64
  0: $t3 := copy($t0)
  1: $t4 := exists<Test::R>($t3)
  2: $t5 := !($t4)
  3: if ($t5) goto 4 else goto 7
  4: label L0
  5: $t6 := 33
  6: abort($t6)
  7: label L2
  8: $t7 := move($t0)
  9: $t8 := borrow_global<Test::R>($t7)
 10: $t1 := $t8
 11: $t9 := copy($t1)
 12: $t10 := borrow_field<Test::R>.v($t9)
 13: $t11 := read_ref($t10)
 14: $t2 := $t11
 15: $t12 := copy($t1)
 16: $t13 := borrow_field<Test::R>.v($t12)
 17: $t14 := read_ref($t13)
 18: $t15 := 1
 19: $t16 := +($t14, $t15)
 20: $t17 := move($t1)
 21: $t18 := borrow_field<Test::R>.v($t17)
 22: write_ref($t18, $t16)
 23: $t19 := move($t2)
 24: return $t19
}


[variant baseline]
fun Test::incr_twice() {
     var $t0: address
     var $t1: u64
     var $t2: address
     var $t3: u64
  0: $t0 := 0x1
  1: $t1 := Test::get_and_incr($t0)
  2: destroy($t1)
  3: $t2 := 0x1
  4: $t3 := Test::get_and_incr($t2)
  5: destroy($t3)
  6: return ()
}

============ after pipeline `spec_instrumentation` ================

[variant verification]
fun Test::get_and_incr($t0|addr: address): u64 {
     var $t1|r: &mut Test::R
     var $t2|v: u64
     var $t3: bool
     var $t4: bool
     var $t5: u64
     var $t6: num
     var $t7: &mut Test::R
     var $t8: u64
     var $t9: u64
     var $t10: u64
     var $t11: u64
     var $t12: &mut u64
  0: assume Neq<address>($t0, 0)
  1: assume CanModify<Test::R>($t0)
  2: @0 := save_mem(Test::R)
  3: $t3 := exists<Test::R>($t0)
  4: $t4 := !($t3)
  5: if ($t4) goto 6 else goto 10
  6: label L0
  7: $t5 := 33
  8: $t6 := move($t5)
  9: goto 27
 10: label L2
     # VC: caller does not have permission to modify `Test::R` at given address at tests/spec_instrumentation/opaque_call.move:8:14+17
 11: assert CanModify<Test::R>($t0)
 12: $t7 := borrow_global<Test::R>($t0) on_abort goto 27 with $t6
 13: $t8 := get_field<Test::R>.v($t7)
 14: $t9 := get_field<Test::R>.v($t7)
 15: $t10 := 1
 16: $t11 := +($t9, $t10) on_abort goto 27 with $t6
 17: $t12 := borrow_field<Test::R>.v($t7)
 18: write_ref($t12, $t11)
 19: write_back[Reference($t7).v (u64)]($t12)
 20: write_back[Test::R@]($t7)
 21: label L3
     # VC: function does not abort under this condition at tests/spec_instrumentation/opaque_call.move:16:6+35
 22: assert Not(Not(exists[@0]<Test::R>($t0)))
     # VC: function does not abort under this condition at tests/spec_instrumentation/opaque_call.move:17:6+56
 23: assert Not(Ge(Add(select Test::R.v(global[@0]<Test::R>($t0)), 1), 18446744073709551615))
     # VC: post-condition does not hold at tests/spec_instrumentation/opaque_call.move:19:6+56
 24: assert Eq<u64>(select Test::R.v(global<Test::R>($t0)), Add(select Test::R.v(global[@0]<Test::R>($t0)), 1))
     # VC: post-condition does not hold at tests/spec_instrumentation/opaque_call.move:20:6+36
 25: assert Eq<u64>($t8, select Test::R.v(global<Test::R>($t0)))
 26: return $t8
 27: label L4
     # VC: abort not covered by any of the `aborts_if` clauses at tests/spec_instrumentation/opaque_call.move:13:2+308
 28: assert Or(Not(exists[@0]<Test::R>($t0)), Ge(Add(select Test::R.v(global[@0]<Test::R>($t0)), 1), 18446744073709551615))
     # VC: abort code not covered by any of the `aborts_if` or `aborts_with` clauses at tests/spec_instrumentation/opaque_call.move:13:2+308
 29: assert Or(And(Not(exists[@0]<Test::R>($t0)), Eq(33, $t6)), Ge(Add(select Test::R.v(global[@0]<Test::R>($t0)), 1), 18446744073709551615))
 30: abort($t6)
}


[variant verification]
fun Test::incr_twice() {
     var $t0: address
     var $t1: u64
     var $t2: bool
     var $t3: num
     var $t4: address
     var $t5: u64
     var $t6: bool
  0: @1 := save_mem(Test::R)
  1: $t0 := 0x1
     # VC: precondition does not hold at this call at tests/spec_instrumentation/opaque_call.move:15:6+22
  2: assert Neq<address>($t0, 0)
  3: $t1 := opaque begin: Test::get_and_incr($t0)
  4: assume Identical($t2, Or(Not(exists<Test::R>($t0)), Ge(Add(select Test::R.v(global<Test::R>($t0)), 1), 18446744073709551615)))
  5: if ($t2) goto 6 else goto 10
  6: label L4
  7: assume Or(And(Not(exists<Test::R>($t0)), Eq(33, $t3)), Ge(Add(select Test::R.v(global<Test::R>($t0)), 1), 18446744073709551615))
  8: trace_abort($t3)
  9: goto 39
 10: label L3
 11: @2 := save_mem(Test::R)
 12: modifies global<Test::R>($t0)
 13: assume WellFormed($t1)
 14: assume Eq<u64>(select Test::R.v(global<Test::R>($t0)), Add(select Test::R.v(global[@2]<Test::R>($t0)), 1))
 15: assume Eq<u64>($t1, select Test::R.v(global<Test::R>($t0)))
 16: $t1 := opaque end: Test::get_and_incr($t0)
 17: destroy($t1)
 18: $t4 := 0x1
     # VC: precondition does not hold at this call at tests/spec_instrumentation/opaque_call.move:15:6+22
 19: assert Neq<address>($t4, 0)
 20: $t5 := opaque begin: Test::get_and_incr($t4)
 21: assume Identical($t6, Or(Not(exists<Test::R>($t4)), Ge(Add(select Test::R.v(global<Test::R>($t4)), 1), 18446744073709551615)))
 22: if ($t6) goto 23 else goto 27
 23: label L6
 24: assume Or(And(Not(exists<Test::R>($t4)), Eq(33, $t3)), Ge(Add(select Test::R.v(global<Test::R>($t4)), 1), 18446744073709551615))
 25: trace_abort($t3)
 26: goto 39
 27: label L5
 28: @3 := save_mem(Test::R)
 29: modifies global<Test::R>($t4)
 30: assume WellFormed($t5)
 31: assume Eq<u64>(select Test::R.v(global<Test::R>($t4)), Add(select Test::R.v(global[@3]<Test::R>($t4)), 1))
 32: assume Eq<u64>($t5, select Test::R.v(global<Test::R>($t4)))
 33: $t5 := opaque end: Test::get_and_incr($t4)
 34: destroy($t5)
 35: label L1
     # VC: function does not abort under this condition at tests/spec_instrumentation/opaque_call.move:28:6+35
 36: assert Not(Not(exists[@1]<Test::R>(1)))
     # VC: post-condition does not hold at tests/spec_instrumentation/opaque_call.move:29:6+56
 37: assert Eq<u64>(select Test::R.v(global<Test::R>(1)), Add(select Test::R.v(global[@1]<Test::R>(1)), 2))
 38: return ()
 39: label L2
     # VC: abort not covered by any of the `aborts_if` clauses at tests/spec_instrumentation/opaque_call.move:27:2+123
 40: assert Not(exists[@1]<Test::R>(1))
     # VC: abort code not covered by any of the `aborts_if` or `aborts_with` clauses at tests/spec_instrumentation/opaque_call.move:27:2+123
 41: assert And(Not(exists[@1]<Test::R>(1)), Eq(33, $t3))
 42: abort($t3)
}



==== spec-instrumenter input specs ====

fun Test::get_and_incr[baseline]
spec {
  requires Neq<address>($t0, 0);
  aborts_if Not(exists<Test::R>($t0));
  aborts_if Ge(Add(select Test::R.v(global<Test::R>($t0)), 1), 18446744073709551615);
  modifies global<Test::R>($t0);
  ensures Eq<u64>(select Test::R.v(global<Test::R>($t0)), Add(select Test::R.v(Old<Test::R>(global<Test::R>($t0))), 1));
  ensures Eq<u64>(result0(), select Test::R.v(global<Test::R>($t0)));
}

fun Test::get_and_incr[verification]
spec {
  requires Neq<address>($t0, 0);
  aborts_if Not(exists<Test::R>($t0));
  aborts_if Ge(Add(select Test::R.v(global<Test::R>($t0)), 1), 18446744073709551615);
  modifies global<Test::R>($t0);
  ensures Eq<u64>(select Test::R.v(global<Test::R>($t0)), Add(select Test::R.v(Old<Test::R>(global<Test::R>($t0))), 1));
  ensures Eq<u64>(result0(), select Test::R.v(global<Test::R>($t0)));
}

fun Test::incr_twice[baseline]
spec {
  aborts_if Not(exists<Test::R>(1));
  ensures Eq<u64>(select Test::R.v(global<Test::R>(1)), Add(select Test::R.v(Old<Test::R>(global<Test::R>(1))), 2));
}

fun Test::incr_twice[verification]
spec {
  aborts_if Not(exists<Test::R>(1));
  ensures Eq<u64>(select Test::R.v(global<Test::R>(1)), Add(select Test::R.v(Old<Test::R>(global<Test::R>(1))), 2));
}