blob: 17c6d974872fc3da74b3c27bb011909c9f643c70 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
; COMMAND-LINE: --finite-model-find
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
(declare-sort $$unsorted 0)
(declare-fun cowlNothing ($$unsorted) Bool)
(declare-fun cowlThing ($$unsorted) Bool)
(declare-fun xsd_integer ($$unsorted) Bool)
(declare-fun xsd_string ($$unsorted) Bool)
(declare-fun _is () $$unsorted)
(assert (and (forall ((X $$unsorted)) (cowlThing X) ) (forall ((X $$unsorted)) (not (cowlNothing X)) )))
(assert (forall ((X $$unsorted)) (= (xsd_string X) (not (xsd_integer X))) ))
(assert (and (forall ((X $$unsorted)) (or (not (cowlThing X)) (= X _is)) ) (cowlThing _is)))
(assert (cowlThing _is))
(assert (and (forall ((X $$unsorted)) (cowlThing X) ) (forall ((X $$unsorted)) (not (cowlNothing X)) ) (forall ((X $$unsorted)) (or (not (cowlThing X)) (= X _is)) )))
(check-sat)
|
