Skip to content

Commit d8d258e

Browse files
committed
Add UNSAT example from issue #115
1 parent 4a5e825 commit d8d258e

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed
Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
(define-fun f () (=> Int Int) (lambda ((loc Int)) 0))
2+
(declare-datatypes () ((S (N) (C (r Int) (e Int)))))
3+
(declare-datatypes () ((T (TT (body S)))))
4+
(define-fun t () T (TT (C 22 5)))
5+
(assert (not (let ((g f)) (= (@ (ite (is-C (body t)) (lambda ((r2 Int)) (ite (= r2 (r (body t))) (e (body t)) (@ g r2))) g) 22) 5))))
6+
(check-sat)

0 commit comments

Comments
 (0)