blob: c04a1ed64ecc7bcfad8d1b2809b88cd067dc5b6b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(set-logic QF_RDL)
(set-info :status unsat)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-sort U 0)
(declare-sort A 2)
(define-sort F (x) (A Real Real))
(declare-fun x2 () (F Real))
(define-fun minus ((x Real) (z Real)) Real (- x z))
(define-fun less ((x Real) (z Real)) Real (< x z))
(define-fun foo ((x Real) (z Real)) Bool (less x z))
(assert (not (=> (foo (minus x y) 0) (less x y))))
(check-sat)
(exit)
|
