/
newton_3_6_false-unreach-call-main-sfxp_16.16_RU_WP.smt2
42 lines (42 loc) · 7.45 KB
/
newton_3_6_false-unreach-call-main-sfxp_16.16_RU_WP.smt2
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
(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 unknown)
(declare-fun |c::main::f::x@1!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::main::1::IN@1!0&0#0| () (_ SFXP 32 16))
(declare-fun |c::main::$tmp::return_value_f$1@1!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::fp::x@1!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::$tmp::return_value_fp$2@1!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::main::1::x@1!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::f::x@2!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::$tmp::return_value_f$3@1!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::fp::x@2!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::$tmp::return_value_fp$4@1!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::main::1::x@1!0&0#2| () (_ SFXP 32 16))
(declare-fun |c::main::f::x@3!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::$tmp::return_value_f$5@1!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::fp::x@3!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::$tmp::return_value_fp$6@1!0&0#1| () (_ SFXP 32 16))
(declare-fun |c::main::main::1::x@1!0&0#3| () (_ SFXP 32 16))
(declare-fun |goto_symex::guard@0!0&0#1| () Bool)
(declare-fun |execution_statet::guard_exec@0!0| () Bool)
(assert (= |c::main::main::1::IN@1!0&0#0| |c::main::f::x@1!0&0#1|))
(assert (let ((a!1 (sfxp.sub wrapAround |c::main::f::x@1!0&0#1| (sfxp.div wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp |c::main::f::x@1!0&0#1| |c::main::f::x@1!0&0#1|) |c::main::f::x@1!0&0#1|) ((_ sfxp 16) #x00060000)))) (a!2 (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp |c::main::f::x@1!0&0#1| |c::main::f::x@1!0&0#1|) |c::main::f::x@1!0&0#1|) |c::main::f::x@1!0&0#1|) |c::main::f::x@1!0&0#1|))) (let ((a!3 (sfxp.add wrapAround (sfxp.add wrapAround a!1 (sfxp.div wrapAround roundUp a!2 ((_ sfxp 16) #x00780000))) (sfxp.div wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp a!2 |c::main::f::x@1!0&0#1|) |c::main::f::x@1!0&0#1|) ((_ sfxp 16) #x13b00000))))) (= a!3 |c::main::$tmp::return_value_f$1@1!0&0#1|))))
(assert (= |c::main::main::1::IN@1!0&0#0| |c::main::fp::x@1!0&0#1|))
(assert (let ((a!1 (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp |c::main::fp::x@1!0&0#1| |c::main::fp::x@1!0&0#1|) |c::main::fp::x@1!0&0#1|) |c::main::fp::x@1!0&0#1|))) (let ((a!2 (sfxp.add wrapAround (sfxp.sub wrapAround ((_ sfxp 16) #x00010000) (sfxp.div wrapAround roundUp (sfxp.mul wrapAround roundUp |c::main::fp::x@1!0&0#1| |c::main::fp::x@1!0&0#1|) ((_ sfxp 16) #x00020000))) (sfxp.div wrapAround roundUp a!1 ((_ sfxp 16) #x00180000))))) (let ((a!3 (sfxp.add wrapAround a!2 (sfxp.div wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp a!1 |c::main::fp::x@1!0&0#1|) |c::main::fp::x@1!0&0#1|) ((_ sfxp 16) #x02d00000))))) (= a!3 |c::main::$tmp::return_value_fp$2@1!0&0#1|)))))
(assert (= (sfxp.sub wrapAround |c::main::main::1::IN@1!0&0#0| (sfxp.div wrapAround roundUp |c::main::$tmp::return_value_f$1@1!0&0#1| |c::main::$tmp::return_value_fp$2@1!0&0#1|)) |c::main::main::1::x@1!0&0#1|))
(assert (= |c::main::main::1::x@1!0&0#1| |c::main::f::x@2!0&0#1|))
(assert (let ((a!1 (sfxp.sub wrapAround |c::main::f::x@2!0&0#1| (sfxp.div wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp |c::main::f::x@2!0&0#1| |c::main::f::x@2!0&0#1|) |c::main::f::x@2!0&0#1|) ((_ sfxp 16) #x00060000)))) (a!2 (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp |c::main::f::x@2!0&0#1| |c::main::f::x@2!0&0#1|) |c::main::f::x@2!0&0#1|) |c::main::f::x@2!0&0#1|) |c::main::f::x@2!0&0#1|))) (let ((a!3 (sfxp.add wrapAround (sfxp.add wrapAround a!1 (sfxp.div wrapAround roundUp a!2 ((_ sfxp 16) #x00780000))) (sfxp.div wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp a!2 |c::main::f::x@2!0&0#1|) |c::main::f::x@2!0&0#1|) ((_ sfxp 16) #x13b00000))))) (= a!3 |c::main::$tmp::return_value_f$3@1!0&0#1|))))
(assert (= |c::main::main::1::x@1!0&0#1| |c::main::fp::x@2!0&0#1|))
(assert (let ((a!1 (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp |c::main::fp::x@2!0&0#1| |c::main::fp::x@2!0&0#1|) |c::main::fp::x@2!0&0#1|) |c::main::fp::x@2!0&0#1|))) (let ((a!2 (sfxp.add wrapAround (sfxp.sub wrapAround ((_ sfxp 16) #x00010000) (sfxp.div wrapAround roundUp (sfxp.mul wrapAround roundUp |c::main::fp::x@2!0&0#1| |c::main::fp::x@2!0&0#1|) ((_ sfxp 16) #x00020000))) (sfxp.div wrapAround roundUp a!1 ((_ sfxp 16) #x00180000))))) (let ((a!3 (sfxp.add wrapAround a!2 (sfxp.div wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp a!1 |c::main::fp::x@2!0&0#1|) |c::main::fp::x@2!0&0#1|) ((_ sfxp 16) #x02d00000))))) (= a!3 |c::main::$tmp::return_value_fp$4@1!0&0#1|)))))
(assert (= (sfxp.sub wrapAround |c::main::main::1::x@1!0&0#1| (sfxp.div wrapAround roundUp |c::main::$tmp::return_value_f$3@1!0&0#1| |c::main::$tmp::return_value_fp$4@1!0&0#1|)) |c::main::main::1::x@1!0&0#2|))
(assert (= |c::main::main::1::x@1!0&0#2| |c::main::f::x@3!0&0#1|))
(assert (let ((a!1 (sfxp.sub wrapAround |c::main::f::x@3!0&0#1| (sfxp.div wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp |c::main::f::x@3!0&0#1| |c::main::f::x@3!0&0#1|) |c::main::f::x@3!0&0#1|) ((_ sfxp 16) #x00060000)))) (a!2 (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp |c::main::f::x@3!0&0#1| |c::main::f::x@3!0&0#1|) |c::main::f::x@3!0&0#1|) |c::main::f::x@3!0&0#1|) |c::main::f::x@3!0&0#1|))) (let ((a!3 (sfxp.add wrapAround (sfxp.add wrapAround a!1 (sfxp.div wrapAround roundUp a!2 ((_ sfxp 16) #x00780000))) (sfxp.div wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp a!2 |c::main::f::x@3!0&0#1|) |c::main::f::x@3!0&0#1|) ((_ sfxp 16) #x13b00000))))) (= a!3 |c::main::$tmp::return_value_f$5@1!0&0#1|))))
(assert (= |c::main::main::1::x@1!0&0#2| |c::main::fp::x@3!0&0#1|))
(assert (let ((a!1 (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp |c::main::fp::x@3!0&0#1| |c::main::fp::x@3!0&0#1|) |c::main::fp::x@3!0&0#1|) |c::main::fp::x@3!0&0#1|))) (let ((a!2 (sfxp.add wrapAround (sfxp.sub wrapAround ((_ sfxp 16) #x00010000) (sfxp.div wrapAround roundUp (sfxp.mul wrapAround roundUp |c::main::fp::x@3!0&0#1| |c::main::fp::x@3!0&0#1|) ((_ sfxp 16) #x00020000))) (sfxp.div wrapAround roundUp a!1 ((_ sfxp 16) #x00180000))))) (let ((a!3 (sfxp.add wrapAround a!2 (sfxp.div wrapAround roundUp (sfxp.mul wrapAround roundUp (sfxp.mul wrapAround roundUp a!1 |c::main::fp::x@3!0&0#1|) |c::main::fp::x@3!0&0#1|) ((_ sfxp 16) #x02d00000))))) (= a!3 |c::main::$tmp::return_value_fp$6@1!0&0#1|)))))
(assert (= (sfxp.sub wrapAround |c::main::main::1::x@1!0&0#2| (sfxp.div wrapAround roundUp |c::main::$tmp::return_value_f$5@1!0&0#1| |c::main::$tmp::return_value_fp$6@1!0&0#1|)) |c::main::main::1::x@1!0&0#3|))
(assert (let ((a!1 (not (not (sfxp.lt |c::main::main::1::x@1!0&0#3| ((_ sfxp 16) #x00001999)))))) (= (not a!1) |goto_symex::guard@0!0&0#1|)))
(assert (let ((a!1 (and (sfxp.gt |c::main::main::1::IN@1!0&0#0| (sfxp.neg wrapAround ((_ sfxp 16) #x00013333))) (sfxp.lt |c::main::main::1::IN@1!0&0#0| ((_ sfxp 16) #x00013333))))) (let ((a!2 (=> (and a!1 (not (not |goto_symex::guard@0!0&0#1|))) false))) (not (=> (and true a!1) (=> |execution_statet::guard_exec@0!0| a!2))))))
(check-sat)
(exit)