blob: 9ccde98cd10d4dd91ad5b1ecad19c4ba6a2279aa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
; COMMAND-LINE: --sygus-inst --no-check-models
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
(declare-datatypes ((a 0))
(((b (c a) (d a)) (n (o a)) (e (f a) (g a)) (h (i (_ BitVec 1))))))
(declare-fun j (a) Bool)
(declare-fun k (a) a)
(declare-fun l () a)
(assert (forall ((m a)) (=> ((_ is h) m) (j (ite ((_ is b) m) (b m m)
(ite ((_ is e) m) (e m m) (ite ((_ is b) m) (e m m) (ite (xor ((_
is n) m) ((_ is e) m)) (b m m) (ite (xor ((_ is n) m) ((_ is n) (o
m))) (k (o m)) (ite ((_ is n) m) m (ite ((_ is h) m) m
l)))))))))))
(check-sat)
|
