Add new tests

Halbaroth · Oct 30, 2024 · 8b134c8 · 8b134c8
1 parent cab2c76
commit 8b134c8
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 0 deletions.
diff --git a/tests/adts/trigger_definition.expected b/tests/adts/trigger_definition.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/adts/trigger_definition.smt2 b/tests/adts/trigger_definition.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(declare-datatype t ((c (b Bool))))
+(declare-fun f (t) Bool)
+(declare-const x t)
+(assert (forall ((y Bool)) (f (c y))))
+(assert (not (f x)))
+(check-sat)
diff --git a/tests/adts/trigger_destructor.expected b/tests/adts/trigger_destructor.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/adts/trigger_destructor.smt2 b/tests/adts/trigger_destructor.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(declare-datatype unit ((void)))
+(declare-datatype t ((box (unbox unit))))
+(declare-fun f (t t) Bool)
+(assert (forall ((u t) (v t)) (f u (box (unbox v)))))
+(assert (not (f (box void) (box void))))
+(check-sat)