Float-to-double2-main-sfxp_16.16_RU_WP.smt2

(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::f@1!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::main::1::d@1!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::main::1::fp@1!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::$tmp::tmp$1@1!0&0#1| () Bool)
(declare-fun |execution_statet::guard_exec@0!0| () Bool)
(assert (= (sfxp.neg wrapAround ((_ sfxp 16) #x00000000)) |c::main::main::1::f@1!0&0#1|))
(assert (= (sfxp.neg wrapAround ((_ sfxp 16) #x00000000)) |c::main::main::1::d@1!0&0#1|))
(assert (= |c::main::main::1::f@1!0&0#1| |c::main::main::1::fp@1!0&0#1|))
(assert (= (= |c::main::main::1::d@1!0&0#1| |c::main::main::1::fp@1!0&0#1|) |c::main::$tmp::tmp$1@1!0&0#1|))
(assert (let ((a!1 (=> true (=> |execution_statet::guard_exec@0!0| (=> (not |c::main::$tmp::tmp$1@1!0&0#1|) false))))) (not a!1)))
(check-sat)
(exit)