blob: cd577add41c7c21c912ff304ed9e74db547c7d6b (
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
|
; COMMAND-LINE: --finite-model-find
; EXPECT: sat
; this problem produced a model where incorrectly card(a)=1 due to --mbqi=fmc
(set-logic ALL)
(declare-sort a 0)
(declare-datatypes ((tree 0)) (((Leaf (lab a)))))
(declare-sort alpha 0)
(declare-fun alphabet (tree a) Bool)
(declare-fun g1 (alpha) tree)
(declare-fun g2 (alpha) a)
(assert
(forall ((x alpha))
(=>
(= (lab (g1 x)) (g2 x))
(alphabet (g1 x) (g2 x)))))
(declare-fun x () a)
(declare-fun y () a)
; (assert (= x y))
(assert
(and
(exists ((b alpha)) (and (= (Leaf y) (g1 b)) (= x (g2 b))))
(not (alphabet (Leaf y) x))))
(check-sat)
|
