Generalize CheckEnum test case to include :prove commands

GaloisInc · Jan 25, 2024 · 8252656 · 8252656
1 parent dd6313c
commit 8252656
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 2 deletions.
diff --git a/tests/enum/CheckEnum.icry b/tests/enum/CheckEnum.icry
diff --git a/tests/enum/CheckEnum.cry → tests/enum/CheckProveEnum.cry b/tests/enum/CheckEnum.cry → tests/enum/CheckProveEnum.cry
diff --git a/tests/enum/CheckProveEnum.icry b/tests/enum/CheckProveEnum.icry
@@ -0,0 +1,10 @@
+:l CheckProveEnum.cry
+:set prover-stats=off
+
+:check
+
+:set prover=sbv-z3
+:prove
+
+:set prover=w4-z3
+:prove
diff --git a/tests/enum/CheckEnum.icry.stdout → tests/enum/CheckProveEnum.icry.stdout b/tests/enum/CheckEnum.icry.stdout → tests/enum/CheckProveEnum.icry.stdout
@@ -13,3 +13,19 @@ Expected test coverage: 0.15% (100 of 65539 values)
 property letterRotateProp Using exhaustive testing.
 Testing... Passed 3 tests.
 Q.E.D.
+:prove maybeMapProp
+	Q.E.D.
+:prove eitherMapProp
+	Q.E.D.
+:prove fooMapProp
+	Q.E.D.
+:prove letterRotateProp
+	Q.E.D.
+:prove maybeMapProp
+	Q.E.D.
+:prove eitherMapProp
+	Q.E.D.
+:prove fooMapProp
+	Q.E.D.
+:prove letterRotateProp
+	Q.E.D.