fixup! motoko-san: add test for arrays + viper lib

serokell · Apr 25, 2024 · 5fb4f45 · 5fb4f45
1 parent 1f03d38
commit 5fb4f45
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/test/viper/ok/nats.silicon.ok b/test/viper/ok/nats.silicon.ok
@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (nats.vpr@2.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@3.1)
diff --git a/test/viper/ok/nats.vpr.ok b/test/viper/ok/nats.vpr.ok
@@ -1,3 +1,4 @@
+import "lib/array.vpr"
 define $Perm($Self) ((true && acc(($Self).x,write)))
 define $Inv($Self) (true)
 method __init__($Self: Ref)