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

[variant baseline]
public fun A::mutate_at($t0|addr: address) {
     var $t1|s: &mut A::S
     var $t2: address
     var $t3: &mut A::S
     var $t4: u64
     var $t5: &mut A::S
     var $t6: &mut u64
  0: $t2 := move($t0)
  1: $t3 := borrow_global<A::S>($t2)
  2: $t1 := $t3
  3: $t4 := 2
  4: $t5 := move($t1)
  5: $t6 := borrow_field<A::S>.x($t5)
  6: write_ref($t6, $t4)
  7: return ()
}


[variant baseline]
public fun A::read_at($t0|addr: address): u64 {
     var $t1|s: &A::S
     var $t2: address
     var $t3: &A::S
     var $t4: &A::S
     var $t5: &u64
     var $t6: u64
  0: $t2 := move($t0)
  1: $t3 := borrow_global<A::S>($t2)
  2: $t1 := $t3
  3: $t4 := move($t1)
  4: $t5 := borrow_field<A::S>.x($t4)
  5: $t6 := read_ref($t5)
  6: return $t6
}


[variant baseline]
public fun B::move_from_test_incorrect($t0|addr1: address, $t1|addr2: address): B::T {
     var $t2|v: B::T
     var $t3|x0: u64
     var $t4|x1: u64
     var $t5: address
     var $t6: u64
     var $t7: address
     var $t8: B::T
     var $t9: address
     var $t10: u64
     var $t11: B::T
  0: $t5 := copy($t1)
  1: $t6 := A::read_at($t5)
  2: $t3 := $t6
  3: $t7 := move($t0)
  4: $t8 := move_from<B::T>($t7)
  5: $t2 := $t8
  6: $t9 := move($t1)
  7: $t10 := A::read_at($t9)
  8: $t4 := $t10
  9: assert Eq<u64>($t3, $t4)
 10: $t11 := move($t2)
 11: return $t11
}


[variant baseline]
public fun B::move_to_test_incorrect($t0|account: &signer, $t1|addr2: address) {
     var $t2|x0: u64
     var $t3|x1: u64
     var $t4: address
     var $t5: u64
     var $t6: &signer
     var $t7: u64
     var $t8: B::T
     var $t9: address
     var $t10: u64
  0: $t4 := copy($t1)
  1: $t5 := A::read_at($t4)
  2: $t2 := $t5
  3: $t6 := move($t0)
  4: $t7 := 2
  5: $t8 := pack B::T($t7)
  6: move_to<B::T>($t8, $t6)
  7: $t9 := move($t1)
  8: $t10 := A::read_at($t9)
  9: $t3 := $t10
 10: assert Eq<u64>($t2, $t3)
 11: return ()
}


[variant baseline]
public fun B::mutate_S_test1_incorrect($t0|addr1: address, $t1|addr2: address) {
     var $t2|x0: u64
     var $t3|x1: u64
     var $t4: address
     var $t5: u64
     var $t6: address
     var $t7: address
     var $t8: u64
  0: $t4 := copy($t1)
  1: $t5 := A::read_at($t4)
  2: $t2 := $t5
  3: $t6 := move($t0)
  4: A::mutate_at($t6)
  5: $t7 := move($t1)
  6: $t8 := A::read_at($t7)
  7: $t3 := $t8
  8: assert Eq<u64>($t2, $t3)
  9: return ()
}


[variant baseline]
public fun B::mutate_S_test2_incorrect($t0|addr: address) {
     var $t1|x0: u64
     var $t2|x1: u64
     var $t3: address
     var $t4: u64
     var $t5: address
     var $t6: address
     var $t7: u64
  0: $t3 := copy($t0)
  1: $t4 := A::read_at($t3)
  2: $t1 := $t4
  3: $t5 := copy($t0)
  4: A::mutate_at($t5)
  5: $t6 := move($t0)
  6: $t7 := A::read_at($t6)
  7: $t2 := $t7
  8: assert Eq<u64>($t1, $t2)
  9: return ()
}


[variant baseline]
public fun B::mutate_at_test_incorrect($t0|addr1: address, $t1|addr2: address) {
     var $t2|t: &mut B::T
     var $t3|x0: u64
     var $t4|x1: u64
     var $t5: address
     var $t6: u64
     var $t7: address
     var $t8: &mut B::T
     var $t9: u64
     var $t10: &mut B::T
     var $t11: &mut u64
     var $t12: address
     var $t13: u64
  0: $t5 := copy($t1)
  1: $t6 := A::read_at($t5)
  2: $t3 := $t6
  3: $t7 := move($t0)
  4: $t8 := borrow_global<B::T>($t7)
  5: $t2 := $t8
  6: $t9 := 2
  7: $t10 := move($t2)
  8: $t11 := borrow_field<B::T>.x($t10)
  9: write_ref($t11, $t9)
 10: $t12 := move($t1)
 11: $t13 := A::read_at($t12)
 12: $t4 := $t13
 13: assert Eq<u64>($t3, $t4)
 14: return ()
}

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

[variant verification]
public fun A::mutate_at($t0|addr: address) {
     var $t1|s: &mut A::S
     var $t2: &mut A::S
     var $t3: num
     var $t4: u64
     var $t5: &mut u64
  0: assume CanModify<A::S>($t0)
  1: @1 := save_mem(A::S)
     # VC: caller does not have permission to modify `A::S` at given address at tests/spec_instrumentation/modifies.move:18:17+17
  2: assert CanModify<A::S>($t0)
  3: $t2 := borrow_global<A::S>($t0) on_abort goto 13 with $t3
  4: $t4 := 2
  5: $t5 := borrow_field<A::S>.x($t2)
  6: write_ref($t5, $t4)
  7: write_back[Reference($t2).x (u64)]($t5)
  8: write_back[A::S@]($t2)
  9: label L1
     # VC: function does not abort under this condition at tests/spec_instrumentation/modifies.move:24:9+27
 10: assert Not(Not(exists[@1]<A::S>($t0)))
     # VC: post-condition does not hold at tests/spec_instrumentation/modifies.move:23:9+31
 11: assert Eq<u64>(select A::S.x(global<A::S>($t0)), 2)
 12: return ()
 13: label L2
     # VC: abort not covered by any of the `aborts_if` clauses at tests/spec_instrumentation/modifies.move:21:5+162
 14: assert Not(exists[@1]<A::S>($t0))
 15: abort($t3)
}


[variant verification]
public fun A::read_at($t0|addr: address): u64 {
     var $t1|s: A::S
     var $t2: A::S
     var $t3: num
     var $t4: u64
  0: @0 := save_mem(A::S)
  1: $t2 := get_global<A::S>($t0) on_abort goto 7 with $t3
  2: $t4 := get_field<A::S>.x($t2)
  3: label L1
     # VC: function does not abort under this condition at tests/spec_instrumentation/modifies.move:13:9+27
  4: assert Not(Not(exists[@0]<A::S>($t0)))
     # VC: post-condition does not hold at tests/spec_instrumentation/modifies.move:14:9+36
  5: assert Eq<u64>($t4, select A::S.x(global<A::S>($t0)))
  6: return $t4
  7: label L2
     # VC: abort not covered by any of the `aborts_if` clauses at tests/spec_instrumentation/modifies.move:11:5+131
  8: assert Not(exists[@0]<A::S>($t0))
  9: abort($t3)
}


[variant verification]
public fun B::move_from_test_incorrect($t0|addr1: address, $t1|addr2: address): B::T {
     var $t2|v: B::T
     var $t3|x0: u64
     var $t4|x1: u64
     var $t5: u64
     var $t6: bool
     var $t7: num
     var $t8: B::T
     var $t9: u64
     var $t10: bool
  0: assume CanModify<B::T>($t1)
  1: $t5 := opaque begin: A::read_at($t1)
  2: assume Identical($t6, Not(exists<A::S>($t1)))
  3: if ($t6) goto 4 else goto 7
  4: label L4
  5: trace_abort($t7)
  6: goto 26
  7: label L3
  8: assume WellFormed($t5)
  9: assume Eq<u64>($t5, select A::S.x(global<A::S>($t1)))
 10: $t5 := opaque end: A::read_at($t1)
     # VC: caller does not have permission to modify `B::T` at given address at tests/spec_instrumentation/modifies.move:65:17+9
 11: assert CanModify<B::T>($t0)
 12: $t8 := move_from<B::T>($t0) on_abort goto 26 with $t7
 13: $t9 := opaque begin: A::read_at($t1)
 14: assume Identical($t10, Not(exists<A::S>($t1)))
 15: if ($t10) goto 16 else goto 19
 16: label L6
 17: trace_abort($t7)
 18: goto 26
 19: label L5
 20: assume WellFormed($t9)
 21: assume Eq<u64>($t9, select A::S.x(global<A::S>($t1)))
 22: $t9 := opaque end: A::read_at($t1)
 23: assert Eq<u64>($t5, $t9)
 24: label L1
 25: return $t8
 26: label L2
 27: abort($t7)
}


[variant verification]
public fun B::move_to_test_incorrect($t0|account: signer, $t1|addr2: address) {
     var $t2|x0: u64
     var $t3|x1: u64
     var $t4: u64
     var $t5: bool
     var $t6: num
     var $t7: u64
     var $t8: B::T
     var $t9: u64
     var $t10: bool
  0: assume CanModify<B::T>($t1)
  1: $t4 := opaque begin: A::read_at($t1)
  2: assume Identical($t5, Not(exists<A::S>($t1)))
  3: if ($t5) goto 4 else goto 7
  4: label L4
  5: trace_abort($t6)
  6: goto 28
  7: label L3
  8: assume WellFormed($t4)
  9: assume Eq<u64>($t4, select A::S.x(global<A::S>($t1)))
 10: $t4 := opaque end: A::read_at($t1)
 11: $t7 := 2
 12: $t8 := pack B::T($t7)
     # VC: caller does not have permission to modify `B::T` at given address at tests/spec_instrumentation/modifies.move:52:9+7
 13: assert CanModify<B::T>($t0)
 14: move_to<B::T>($t8, $t0) on_abort goto 28 with $t6
 15: $t9 := opaque begin: A::read_at($t1)
 16: assume Identical($t10, Not(exists<A::S>($t1)))
 17: if ($t10) goto 18 else goto 21
 18: label L6
 19: trace_abort($t6)
 20: goto 28
 21: label L5
 22: assume WellFormed($t9)
 23: assume Eq<u64>($t9, select A::S.x(global<A::S>($t1)))
 24: $t9 := opaque end: A::read_at($t1)
 25: assert Eq<u64>($t4, $t9)
 26: label L1
 27: return ()
 28: label L2
 29: abort($t6)
}


[variant verification]
public fun B::mutate_S_test1_incorrect($t0|addr1: address, $t1|addr2: address) {
     var $t2|x0: u64
     var $t3|x1: u64
     var $t4: u64
     var $t5: bool
     var $t6: num
     var $t7: bool
     var $t8: u64
     var $t9: bool
  0: assume Neq<address>($t0, $t1)
  1: assume CanModify<A::S>($t1)
  2: $t4 := opaque begin: A::read_at($t1)
  3: assume Identical($t5, Not(exists<A::S>($t1)))
  4: if ($t5) goto 5 else goto 8
  5: label L4
  6: trace_abort($t6)
  7: goto 36
  8: label L3
  9: assume WellFormed($t4)
 10: assume Eq<u64>($t4, select A::S.x(global<A::S>($t1)))
 11: $t4 := opaque end: A::read_at($t1)
     # VC: caller does not have permission to modify `A::S` at given address at tests/spec_instrumentation/modifies.move:79:9+19
 12: assert CanModify<A::S>($t0)
 13: opaque begin: A::mutate_at($t0)
 14: assume Identical($t7, Not(exists<A::S>($t0)))
 15: if ($t7) goto 16 else goto 19
 16: label L6
 17: trace_abort($t6)
 18: goto 36
 19: label L5
 20: modifies global<A::S>($t0)
 21: assume Eq<u64>(select A::S.x(global<A::S>($t0)), 2)
 22: opaque end: A::mutate_at($t0)
 23: $t8 := opaque begin: A::read_at($t1)
 24: assume Identical($t9, Not(exists<A::S>($t1)))
 25: if ($t9) goto 26 else goto 29
 26: label L8
 27: trace_abort($t6)
 28: goto 36
 29: label L7
 30: assume WellFormed($t8)
 31: assume Eq<u64>($t8, select A::S.x(global<A::S>($t1)))
 32: $t8 := opaque end: A::read_at($t1)
 33: assert Eq<u64>($t4, $t8)
 34: label L1
 35: return ()
 36: label L2
 37: abort($t6)
}


[variant verification]
public fun B::mutate_S_test2_incorrect($t0|addr: address) {
     var $t1|x0: u64
     var $t2|x1: u64
     var $t3: u64
     var $t4: bool
     var $t5: num
     var $t6: bool
     var $t7: u64
     var $t8: bool
  0: assume CanModify<A::S>($t0)
  1: $t3 := opaque begin: A::read_at($t0)
  2: assume Identical($t4, Not(exists<A::S>($t0)))
  3: if ($t4) goto 4 else goto 7
  4: label L4
  5: trace_abort($t5)
  6: goto 35
  7: label L3
  8: assume WellFormed($t3)
  9: assume Eq<u64>($t3, select A::S.x(global<A::S>($t0)))
 10: $t3 := opaque end: A::read_at($t0)
     # VC: caller does not have permission to modify `A::S` at given address at tests/spec_instrumentation/modifies.move:92:9+18
 11: assert CanModify<A::S>($t0)
 12: opaque begin: A::mutate_at($t0)
 13: assume Identical($t6, Not(exists<A::S>($t0)))
 14: if ($t6) goto 15 else goto 18
 15: label L6
 16: trace_abort($t5)
 17: goto 35
 18: label L5
 19: modifies global<A::S>($t0)
 20: assume Eq<u64>(select A::S.x(global<A::S>($t0)), 2)
 21: opaque end: A::mutate_at($t0)
 22: $t7 := opaque begin: A::read_at($t0)
 23: assume Identical($t8, Not(exists<A::S>($t0)))
 24: if ($t8) goto 25 else goto 28
 25: label L8
 26: trace_abort($t5)
 27: goto 35
 28: label L7
 29: assume WellFormed($t7)
 30: assume Eq<u64>($t7, select A::S.x(global<A::S>($t0)))
 31: $t7 := opaque end: A::read_at($t0)
 32: assert Eq<u64>($t3, $t7)
 33: label L1
 34: return ()
 35: label L2
 36: abort($t5)
}


[variant verification]
public fun B::mutate_at_test_incorrect($t0|addr1: address, $t1|addr2: address) {
     var $t2|t: &mut B::T
     var $t3|x0: u64
     var $t4|x1: u64
     var $t5: u64
     var $t6: bool
     var $t7: num
     var $t8: &mut B::T
     var $t9: u64
     var $t10: &mut u64
     var $t11: u64
     var $t12: bool
  0: assume CanModify<B::T>($t1)
  1: $t5 := opaque begin: A::read_at($t1)
  2: assume Identical($t6, Not(exists<A::S>($t1)))
  3: if ($t6) goto 4 else goto 7
  4: label L4
  5: trace_abort($t7)
  6: goto 31
  7: label L3
  8: assume WellFormed($t5)
  9: assume Eq<u64>($t5, select A::S.x(global<A::S>($t1)))
 10: $t5 := opaque end: A::read_at($t1)
     # VC: caller does not have permission to modify `B::T` at given address at tests/spec_instrumentation/modifies.move:38:17+17
 11: assert CanModify<B::T>($t0)
 12: $t8 := borrow_global<B::T>($t0) on_abort goto 31 with $t7
 13: $t9 := 2
 14: $t10 := borrow_field<B::T>.x($t8)
 15: write_ref($t10, $t9)
 16: write_back[Reference($t8).x (u64)]($t10)
 17: write_back[B::T@]($t8)
 18: $t11 := opaque begin: A::read_at($t1)
 19: assume Identical($t12, Not(exists<A::S>($t1)))
 20: if ($t12) goto 21 else goto 24
 21: label L6
 22: trace_abort($t7)
 23: goto 31
 24: label L5
 25: assume WellFormed($t11)
 26: assume Eq<u64>($t11, select A::S.x(global<A::S>($t1)))
 27: $t11 := opaque end: A::read_at($t1)
 28: assert Eq<u64>($t5, $t11)
 29: label L1
 30: return ()
 31: label L2
 32: abort($t7)
}



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

fun A::mutate_at[baseline]
spec {
  ensures Eq<u64>(select A::S.x(global<A::S>($t0)), 2);
  aborts_if Not(exists<A::S>($t0));
  modifies global<A::S>($t0);
}

fun A::mutate_at[verification]
spec {
  ensures Eq<u64>(select A::S.x(global<A::S>($t0)), 2);
  aborts_if Not(exists<A::S>($t0));
  modifies global<A::S>($t0);
}

fun A::read_at[baseline]
spec {
  aborts_if Not(exists<A::S>($t0));
  ensures Eq<u64>(result0(), select A::S.x(global<A::S>($t0)));
}

fun A::read_at[verification]
spec {
  aborts_if Not(exists<A::S>($t0));
  ensures Eq<u64>(result0(), select A::S.x(global<A::S>($t0)));
}

fun B::move_from_test_incorrect[baseline]
spec {
  modifies global<B::T>($t1);
}

fun B::move_from_test_incorrect[verification]
spec {
  modifies global<B::T>($t1);
}

fun B::move_to_test_incorrect[baseline]
spec {
  modifies global<B::T>($t1);
}

fun B::move_to_test_incorrect[verification]
spec {
  modifies global<B::T>($t1);
}

fun B::mutate_S_test1_incorrect[baseline]
spec {
  requires Neq<address>($t0, $t1);
  modifies global<A::S>($t1);
}

fun B::mutate_S_test1_incorrect[verification]
spec {
  requires Neq<address>($t0, $t1);
  modifies global<A::S>($t1);
}

fun B::mutate_S_test2_incorrect[baseline]
spec {
  modifies global<A::S>($t0);
}

fun B::mutate_S_test2_incorrect[verification]
spec {
  modifies global<A::S>($t0);
}

fun B::mutate_at_test_incorrect[baseline]
spec {
  modifies global<B::T>($t1);
}

fun B::mutate_at_test_incorrect[verification]
spec {
  modifies global<B::T>($t1);
}