blob: 29e28b0e9b72ac03c7ec0b01c5369ebae844d446 (
plain)
1
2
3
4
5
6
7
8
9
|
(set-logic QF_UFLIA)
(declare-fun op_4 () Int)
(declare-fun op_1 (Int) Bool)
(declare-fun op_0 () Int)
(declare-fun op_2 () Int)
(declare-fun op_3 (Int) Int)
(assert (and (= op_2 op_4) (and (= op_0 op_4) (or (not (= (op_3 op_2) (op_3 op_0))) (and (op_1 op_2) (not (op_1 op_0)))))))
(check-sat)
(exit)
|
