-
Notifications
You must be signed in to change notification settings - Fork 0
/
Float5-main-sfxp_16.16_RU_ST.smt2
16 lines (16 loc) · 1.29 KB
/
Float5-main-sfxp_16.16_RU_ST.smt2
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
(set-info :smt-lib-version 2.6)
(set-logic QF_FXP)
(set-info :source |ESBMC floating-point test cases contributed by Mikhail Ramalho.|)
(set-info :category "crafted")
(set-info :status unsat)
(declare-fun |c::main::main::1::b@1!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::main::1::a@1!0&0#0| () (_ SFXP 32 16))
(declare-fun |c::main::main::1::a@1!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::main::1::a@1!0&0#2| () (_ SFXP 32 16))
(declare-fun |execution_statet::guard_exec@0!0| () Bool)
(assert (= |c::main::main::1::a@1!0&0#0| |c::main::main::1::b@1!0&0#1|))
(assert (= (sfxp.div saturation roundUp |c::main::main::1::a@1!0&0#0| ((_ sfxp 16) #x00020000)) |c::main::main::1::a@1!0&0#1|))
(assert (= (sfxp.mul saturation roundUp |c::main::main::1::a@1!0&0#1| ((_ sfxp 16) #x00020000)) |c::main::main::1::a@1!0&0#2|))
(assert (let ((a!1 (or (= |c::main::main::1::a@1!0&0#0| ((_ sfxp 16) #x00010000)) (= |c::main::main::1::a@1!0&0#0| ((_ sfxp 16) #x00008000)) (= |c::main::main::1::a@1!0&0#0| ((_ sfxp 16) #x00020000)) (= |c::main::main::1::a@1!0&0#0| ((_ sfxp 16) #x00030000)) (= |c::main::main::1::a@1!0&0#0| ((_ sfxp 16) #x00001999))))) (let ((a!2 (=> (and true a!1) (=> |execution_statet::guard_exec@0!0| (=> a!1 (= |c::main::main::1::a@1!0&0#2| |c::main::main::1::b@1!0&0#1|)))))) (not a!2))))
(check-sat)
(exit)