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

test: proper smtlib for QFUF problems

Browse source
This commit is contained in:
Simon Cruanes 2018-06-11 21:56:34 -05:00
parent 5e380464ce
commit c5f23e32b9
2 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/sat/test-007.smt2
View file

@ -1,2 +1,6 @@
(declare-sort $i 0)
(declare-fun a () $i)
(declare-fun b () $i)
(declare-fun c () $i)
(assert (and (= a b) (= b c))) (assert (and (= a b) (= b c)))
(check-sat) (check-sat)

5
tests/sat/test-010.smt2
View file

@ -1,2 +1,7 @@
(declare-sort $i 0)
(declare-fun a () $i)
(declare-fun b () $i)
(declare-fun c () $i)
(declare-fun d () $i)
(assert (and (= a b) (= b c) (or (not (= a c)) (= a d)))) (assert (and (= a b) (= b c) (or (not (= a c)) (= a d))))
(check-sat) (check-sat)