blob: 4648c327ad8b32405b355bc729660b38f547bc34 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
; COMMAND-LINE: --decision=internal -q
; COMMAND-LINE: --decision=justification -q
; EXPECT: sat
(set-info :smt-lib-version 2.6)
(set-logic QF_BVFP)
(declare-fun a () (_ BitVec 64))
(declare-fun b () (_ BitVec 64))
(assert (fp.leq ((_ to_fp 11 53) a) ((_ to_fp 11 53) (_ bv4626322717216342016 64))))
(assert (not (fp.isNaN ((_ to_fp 11 53) b))))
(declare-fun k2 () (_ BitVec 64))
(assert (or (= k2 b) (= k2 a)))
(assert
(or (fp.isNaN ((_ to_fp 11 53) k2)) (fp.gt ((_ to_fp 11 53) k2) ((_ to_fp 11 53) (_ bv4626322717216342016 64))) ))
(check-sat)
|
