blob: 317f755d8c2fc4e57750b5b4d96724f44e8566fe (
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)
(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)
|
