update prover tests

aptos-labs · Oct 1, 2024 · daea4f8 · daea4f8
1 parent cad200d
commit daea4f8
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 7 deletions.
diff --git a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.exp b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.exp
@@ -104,8 +104,8 @@ error: unknown assertion failed
    =     at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =         b = <redacted>
-   =         a = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
+   =         a = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =         i = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:86: nested_loop2

diff --git a/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp b/third_party/move/move-prover/tests/sources/functional/loops_with_memory_ops.v2_exp
@@ -42,8 +42,8 @@ error: induction case of the loop invariant does not hold
    =     at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =         a = <redacted>
-   =         b = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
+   =         b = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =         <redacted> = <redacted>
    =         i = <redacted>
@@ -100,8 +100,6 @@ error: unknown assertion failed
    =     at tests/sources/functional/loops_with_memory_ops.move:75: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
    =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
-   =         a = <redacted>
-   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
    =         b = <redacted>
    =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
    =         <redacted> = <redacted>

diff --git a/third_party/move/move-prover/tests/sources/functional/trace.exp b/third_party/move/move-prover/tests/sources/functional/trace.exp
@@ -47,7 +47,7 @@ error: post-condition does not hold
    │
    = Related Global Memory:
    =         Resource name: TestTracing_R
-   =         Values:  {Address(18467): <redacted>, Default: TestTracing.R{x = 4}}
+   =         Values:  {Address(6334): <redacted>, Default: empty}
    = Related Bindings:
    =         addr = <redacted>
    =         exists<R>(addr) = <redacted>
@@ -74,7 +74,7 @@ error: global memory invariant does not hold
    │
    = Related Global Memory:
    =         Resource name: TestTracing_R
-   =         Values:  {Address(0): <redacted>, Default: TestTracing.R{x = 5}}
+   =         Values:  {Address(0): <redacted>, Default: empty}
    =     at tests/sources/functional/trace.move:29: publish_invalid
    =     at tests/sources/functional/trace.move:33: publish_invalid (spec)
    =         `let addr = signer::address_of(s);` = <redacted>

diff --git a/third_party/move/move-prover/tests/sources/functional/trace.v2_exp b/third_party/move/move-prover/tests/sources/functional/trace.v2_exp
@@ -47,7 +47,7 @@ error: post-condition does not hold
    │
    = Related Global Memory:
    =         Resource name: TestTracing_R
-   =         Values:  {Address(18467): <redacted>, Default: empty}
+   =         Values:  {Address(6334): <redacted>, Default: empty}
    = Related Bindings:
    =         addr = <redacted>
    =         exists<R>(addr) = <redacted>