simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-05 19:00:33 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

test: add some basic datatype tests

Browse source
This commit is contained in:
Simon Cruanes 2019-12-01 17:38:24 -06:00
parent 444a0b9f85
commit c55e7a613b
3 changed files with 33 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
tests/unsat/data_acycl1.smt2 Normal file
View file

@ -0,0 +1,8 @@
(set-info :status unsat)
(declare-datatypes ((nat 0)) (((Z) (S (pred nat)))))
(declare-const n nat)
(assert (= n (S (S n))))
(check-sat)

14
tests/unsat/data_acycl_if.smt2 Normal file
View file

@ -0,0 +1,14 @@
(set-info :status unsat)
(declare-datatypes ((nat 0)) (((Z) (S (pred nat)))))
(declare-const p Bool)
(declare-const n nat)
(declare-const n_t nat)
(declare-const n_f nat)
(assert (= n_t (S n)))
(assert (= n_f (S (S n))))
(assert (=> p (= n (S n_t))))
(assert (=> (not p) (= n (S n_f))))
(check-sat)

11
tests/unsat/data_card1.smt2 Normal file
View file

@ -0,0 +1,11 @@
(set-info :status unsat)
(declare-datatypes ((three 0)) (((A) (B) (C))))
(declare-const t1 three)
(declare-const t2 three)
(declare-const t3 three)
(declare-const t4 three)
(assert (distinct t1 t2 t3 t4))
(check-sat)