Add SpriteHornPosTest>>testL8uniqueVoid

shingarov · Sep 12, 2024 · 7d54000 · 7d54000
1 parent 58653ef
commit 7d54000
Showing 1 changed file with 15 additions and 0 deletions.
diff --git a/src/SpriteLang-Tests/SpriteHornPosTest.class.st b/src/SpriteLang-Tests/SpriteHornPosTest.class.st
@@ -1630,3 +1630,18 @@ SpriteHornPosTest >> testL7sumAcc [
                    & (v < n))))))))))))))
 '
 ]
+
+{ #category : #'tests-L8' }
+SpriteHornPosTest >> testL8uniqueVoid [
+	"Cf. liquid-fixpoint/doodles/L8uniqueVoid.smt2 on branch experiment-z3datatypes"
+	self provePos: '
+(data V 0 = [
+        | Nil {}
+      ])
+ 
+(constraint
+    (forall ((a V) (Bool true))
+      (forall ((b V) (Bool true))
+          ((a === b)))))
+'
+]