blob: 35110d831d4283d686140d3af77e5e9fab73a368 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
(set-info :status sat)
; Observed behavior
;
; Benchmark taking too long. Lemmas being generated indefinitely with
; skolems due to the "two sets not being equal" axiom.
;
; What was the bug?
;
;
(define-sort Elt () Int)
(define-sort mySet () (Set Elt))
(declare-fun f (Int) mySet)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun S () mySet)
(declare-fun T () mySet)
(assert (= (f x)
(union S T)))
(assert (= (f x)
(union T (f y))))
(assert (not (= (f y)
(union T (f y)))))
(check-sat)
|
