Closed
Description
I wish I had a smaller benchmark to report; and I'm working on generating one. The following benchmark results in an incorrect value reported by z3. In particular, this seems to be a regression, since z3 compiled on August 17th of this year produces the following correct answer:
sat
(objectives
(s241 8388607)
)
((s0 (fp #b1 #xfe #b00001100001010001010000)))
((s1 (fp #b1 #xfe #b00001100001010001010000)))
((s14 #xff800000))
((s241 #x007fffff))
But a freshly compiled z3 produces the incorrect result:
sat
(objectives
(s241 0)
)
((s0 (_ -zero 8 24)))
((s1 (_ +zero 8 24)))
((s14 #x00000000))
((s241 #x80000000))
The idea is that s0 and s1 are floating-point values such that s0+s1 is still a valid float (i.e., not -oo), but is also minimal.
I'm posting this with the hopes that you can replicate and perhaps bisect to find the culprit. I'll continue trying to find a smaller example if I can.
Here's the benchmark:
(set-option :produce-models true)
(set-logic QF_FPBV)
(define-fun s13 () (_ BitVec 32) #x80000000)
(define-fun s18 () (_ BitVec 1) #b0)
(define-fun s145 () (_ BitVec 32) #x00000001)
(define-fun s146 () (_ BitVec 32) #x00000000)
(define-fun s148 () (_ BitVec 32) #x00000002)
(define-fun s151 () (_ BitVec 32) #x00000004)
(define-fun s154 () (_ BitVec 32) #x00000008)
(define-fun s157 () (_ BitVec 32) #x00000010)
(define-fun s160 () (_ BitVec 32) #x00000020)
(define-fun s163 () (_ BitVec 32) #x00000040)
(define-fun s166 () (_ BitVec 32) #x00000080)
(define-fun s169 () (_ BitVec 32) #x00000100)
(define-fun s172 () (_ BitVec 32) #x00000200)
(define-fun s175 () (_ BitVec 32) #x00000400)
(define-fun s178 () (_ BitVec 32) #x00000800)
(define-fun s181 () (_ BitVec 32) #x00001000)
(define-fun s184 () (_ BitVec 32) #x00002000)
(define-fun s187 () (_ BitVec 32) #x00004000)
(define-fun s190 () (_ BitVec 32) #x00008000)
(define-fun s193 () (_ BitVec 32) #x00010000)
(define-fun s196 () (_ BitVec 32) #x00020000)
(define-fun s199 () (_ BitVec 32) #x00040000)
(define-fun s202 () (_ BitVec 32) #x00080000)
(define-fun s205 () (_ BitVec 32) #x00100000)
(define-fun s208 () (_ BitVec 32) #x00200000)
(define-fun s211 () (_ BitVec 32) #x00400000)
(define-fun s214 () (_ BitVec 32) #x00800000)
(define-fun s217 () (_ BitVec 32) #x01000000)
(define-fun s220 () (_ BitVec 32) #x02000000)
(define-fun s223 () (_ BitVec 32) #x04000000)
(define-fun s226 () (_ BitVec 32) #x08000000)
(define-fun s229 () (_ BitVec 32) #x10000000)
(define-fun s232 () (_ BitVec 32) #x20000000)
(define-fun s235 () (_ BitVec 32) #x40000000)
(declare-fun s0 () (_ FloatingPoint 8 24))
(declare-fun s1 () (_ FloatingPoint 8 24))
(declare-fun s14 () (_ BitVec 32)) ; tracks user variable "__internal_sbv_s14"
(declare-fun s241 () (_ BitVec 32)) ; tracks m
(define-fun s2 () Bool (fp.isNaN s0))
(define-fun s3 () Bool (fp.isInfinite s0))
(define-fun s4 () Bool (or s2 s3))
(define-fun s5 () Bool (not s4))
(define-fun s6 () Bool (fp.eq s0 s1))
(define-fun s7 () (_ FloatingPoint 8 24) (fp.add roundNearestTiesToEven s0 s1))
(define-fun s8 () Bool (fp.isNaN s7))
(define-fun s9 () Bool (not s8))
(define-fun s10 () Bool (fp.isZero s7))
(define-fun s11 () Bool (fp.isNegative s7))
(define-fun s12 () Bool (and s10 s11))
(define-fun s15 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) s14))
(define-fun s16 () Bool (= s7 s15))
(define-fun s17 () (_ BitVec 1) ((_ extract 31 31) s14))
(define-fun s19 () Bool (distinct s17 s18))
(define-fun s20 () Bool (not s19))
(define-fun s21 () (_ BitVec 1) ((_ extract 30 30) s14))
(define-fun s22 () Bool (distinct s18 s21))
(define-fun s23 () Bool (not s22))
(define-fun s24 () Bool (ite s19 s23 s22))
(define-fun s25 () (_ BitVec 1) ((_ extract 29 29) s14))
(define-fun s26 () Bool (distinct s18 s25))
(define-fun s27 () Bool (not s26))
(define-fun s28 () Bool (ite s19 s27 s26))
(define-fun s29 () (_ BitVec 1) ((_ extract 28 28) s14))
(define-fun s30 () Bool (distinct s18 s29))
(define-fun s31 () Bool (not s30))
(define-fun s32 () Bool (ite s19 s31 s30))
(define-fun s33 () (_ BitVec 1) ((_ extract 27 27) s14))
(define-fun s34 () Bool (distinct s18 s33))
(define-fun s35 () Bool (not s34))
(define-fun s36 () Bool (ite s19 s35 s34))
(define-fun s37 () (_ BitVec 1) ((_ extract 26 26) s14))
(define-fun s38 () Bool (distinct s18 s37))
(define-fun s39 () Bool (not s38))
(define-fun s40 () Bool (ite s19 s39 s38))
(define-fun s41 () (_ BitVec 1) ((_ extract 25 25) s14))
(define-fun s42 () Bool (distinct s18 s41))
(define-fun s43 () Bool (not s42))
(define-fun s44 () Bool (ite s19 s43 s42))
(define-fun s45 () (_ BitVec 1) ((_ extract 24 24) s14))
(define-fun s46 () Bool (distinct s18 s45))
(define-fun s47 () Bool (not s46))
(define-fun s48 () Bool (ite s19 s47 s46))
(define-fun s49 () (_ BitVec 1) ((_ extract 23 23) s14))
(define-fun s50 () Bool (distinct s18 s49))
(define-fun s51 () Bool (not s50))
(define-fun s52 () Bool (ite s19 s51 s50))
(define-fun s53 () (_ BitVec 1) ((_ extract 22 22) s14))
(define-fun s54 () Bool (distinct s18 s53))
(define-fun s55 () Bool (not s54))
(define-fun s56 () Bool (ite s19 s55 s54))
(define-fun s57 () (_ BitVec 1) ((_ extract 21 21) s14))
(define-fun s58 () Bool (distinct s18 s57))
(define-fun s59 () Bool (not s58))
(define-fun s60 () Bool (ite s19 s59 s58))
(define-fun s61 () (_ BitVec 1) ((_ extract 20 20) s14))
(define-fun s62 () Bool (distinct s18 s61))
(define-fun s63 () Bool (not s62))
(define-fun s64 () Bool (ite s19 s63 s62))
(define-fun s65 () (_ BitVec 1) ((_ extract 19 19) s14))
(define-fun s66 () Bool (distinct s18 s65))
(define-fun s67 () Bool (not s66))
(define-fun s68 () Bool (ite s19 s67 s66))
(define-fun s69 () (_ BitVec 1) ((_ extract 18 18) s14))
(define-fun s70 () Bool (distinct s18 s69))
(define-fun s71 () Bool (not s70))
(define-fun s72 () Bool (ite s19 s71 s70))
(define-fun s73 () (_ BitVec 1) ((_ extract 17 17) s14))
(define-fun s74 () Bool (distinct s18 s73))
(define-fun s75 () Bool (not s74))
(define-fun s76 () Bool (ite s19 s75 s74))
(define-fun s77 () (_ BitVec 1) ((_ extract 16 16) s14))
(define-fun s78 () Bool (distinct s18 s77))
(define-fun s79 () Bool (not s78))
(define-fun s80 () Bool (ite s19 s79 s78))
(define-fun s81 () (_ BitVec 1) ((_ extract 15 15) s14))
(define-fun s82 () Bool (distinct s18 s81))
(define-fun s83 () Bool (not s82))
(define-fun s84 () Bool (ite s19 s83 s82))
(define-fun s85 () (_ BitVec 1) ((_ extract 14 14) s14))
(define-fun s86 () Bool (distinct s18 s85))
(define-fun s87 () Bool (not s86))
(define-fun s88 () Bool (ite s19 s87 s86))
(define-fun s89 () (_ BitVec 1) ((_ extract 13 13) s14))
(define-fun s90 () Bool (distinct s18 s89))
(define-fun s91 () Bool (not s90))
(define-fun s92 () Bool (ite s19 s91 s90))
(define-fun s93 () (_ BitVec 1) ((_ extract 12 12) s14))
(define-fun s94 () Bool (distinct s18 s93))
(define-fun s95 () Bool (not s94))
(define-fun s96 () Bool (ite s19 s95 s94))
(define-fun s97 () (_ BitVec 1) ((_ extract 11 11) s14))
(define-fun s98 () Bool (distinct s18 s97))
(define-fun s99 () Bool (not s98))
(define-fun s100 () Bool (ite s19 s99 s98))
(define-fun s101 () (_ BitVec 1) ((_ extract 10 10) s14))
(define-fun s102 () Bool (distinct s18 s101))
(define-fun s103 () Bool (not s102))
(define-fun s104 () Bool (ite s19 s103 s102))
(define-fun s105 () (_ BitVec 1) ((_ extract 9 9) s14))
(define-fun s106 () Bool (distinct s18 s105))
(define-fun s107 () Bool (not s106))
(define-fun s108 () Bool (ite s19 s107 s106))
(define-fun s109 () (_ BitVec 1) ((_ extract 8 8) s14))
(define-fun s110 () Bool (distinct s18 s109))
(define-fun s111 () Bool (not s110))
(define-fun s112 () Bool (ite s19 s111 s110))
(define-fun s113 () (_ BitVec 1) ((_ extract 7 7) s14))
(define-fun s114 () Bool (distinct s18 s113))
(define-fun s115 () Bool (not s114))
(define-fun s116 () Bool (ite s19 s115 s114))
(define-fun s117 () (_ BitVec 1) ((_ extract 6 6) s14))
(define-fun s118 () Bool (distinct s18 s117))
(define-fun s119 () Bool (not s118))
(define-fun s120 () Bool (ite s19 s119 s118))
(define-fun s121 () (_ BitVec 1) ((_ extract 5 5) s14))
(define-fun s122 () Bool (distinct s18 s121))
(define-fun s123 () Bool (not s122))
(define-fun s124 () Bool (ite s19 s123 s122))
(define-fun s125 () (_ BitVec 1) ((_ extract 4 4) s14))
(define-fun s126 () Bool (distinct s18 s125))
(define-fun s127 () Bool (not s126))
(define-fun s128 () Bool (ite s19 s127 s126))
(define-fun s129 () (_ BitVec 1) ((_ extract 3 3) s14))
(define-fun s130 () Bool (distinct s18 s129))
(define-fun s131 () Bool (not s130))
(define-fun s132 () Bool (ite s19 s131 s130))
(define-fun s133 () (_ BitVec 1) ((_ extract 2 2) s14))
(define-fun s134 () Bool (distinct s18 s133))
(define-fun s135 () Bool (not s134))
(define-fun s136 () Bool (ite s19 s135 s134))
(define-fun s137 () (_ BitVec 1) ((_ extract 1 1) s14))
(define-fun s138 () Bool (distinct s18 s137))
(define-fun s139 () Bool (not s138))
(define-fun s140 () Bool (ite s19 s139 s138))
(define-fun s141 () (_ BitVec 1) ((_ extract 0 0) s14))
(define-fun s142 () Bool (distinct s18 s141))
(define-fun s143 () Bool (not s142))
(define-fun s144 () Bool (ite s19 s143 s142))
(define-fun s147 () (_ BitVec 32) (ite s144 s145 s146))
(define-fun s149 () (_ BitVec 32) (bvor s147 s148))
(define-fun s150 () (_ BitVec 32) (ite s140 s149 s147))
(define-fun s152 () (_ BitVec 32) (bvor s150 s151))
(define-fun s153 () (_ BitVec 32) (ite s136 s152 s150))
(define-fun s155 () (_ BitVec 32) (bvor s153 s154))
(define-fun s156 () (_ BitVec 32) (ite s132 s155 s153))
(define-fun s158 () (_ BitVec 32) (bvor s156 s157))
(define-fun s159 () (_ BitVec 32) (ite s128 s158 s156))
(define-fun s161 () (_ BitVec 32) (bvor s159 s160))
(define-fun s162 () (_ BitVec 32) (ite s124 s161 s159))
(define-fun s164 () (_ BitVec 32) (bvor s162 s163))
(define-fun s165 () (_ BitVec 32) (ite s120 s164 s162))
(define-fun s167 () (_ BitVec 32) (bvor s165 s166))
(define-fun s168 () (_ BitVec 32) (ite s116 s167 s165))
(define-fun s170 () (_ BitVec 32) (bvor s168 s169))
(define-fun s171 () (_ BitVec 32) (ite s112 s170 s168))
(define-fun s173 () (_ BitVec 32) (bvor s171 s172))
(define-fun s174 () (_ BitVec 32) (ite s108 s173 s171))
(define-fun s176 () (_ BitVec 32) (bvor s174 s175))
(define-fun s177 () (_ BitVec 32) (ite s104 s176 s174))
(define-fun s179 () (_ BitVec 32) (bvor s177 s178))
(define-fun s180 () (_ BitVec 32) (ite s100 s179 s177))
(define-fun s182 () (_ BitVec 32) (bvor s180 s181))
(define-fun s183 () (_ BitVec 32) (ite s96 s182 s180))
(define-fun s185 () (_ BitVec 32) (bvor s183 s184))
(define-fun s186 () (_ BitVec 32) (ite s92 s185 s183))
(define-fun s188 () (_ BitVec 32) (bvor s186 s187))
(define-fun s189 () (_ BitVec 32) (ite s88 s188 s186))
(define-fun s191 () (_ BitVec 32) (bvor s189 s190))
(define-fun s192 () (_ BitVec 32) (ite s84 s191 s189))
(define-fun s194 () (_ BitVec 32) (bvor s192 s193))
(define-fun s195 () (_ BitVec 32) (ite s80 s194 s192))
(define-fun s197 () (_ BitVec 32) (bvor s195 s196))
(define-fun s198 () (_ BitVec 32) (ite s76 s197 s195))
(define-fun s200 () (_ BitVec 32) (bvor s198 s199))
(define-fun s201 () (_ BitVec 32) (ite s72 s200 s198))
(define-fun s203 () (_ BitVec 32) (bvor s201 s202))
(define-fun s204 () (_ BitVec 32) (ite s68 s203 s201))
(define-fun s206 () (_ BitVec 32) (bvor s204 s205))
(define-fun s207 () (_ BitVec 32) (ite s64 s206 s204))
(define-fun s209 () (_ BitVec 32) (bvor s207 s208))
(define-fun s210 () (_ BitVec 32) (ite s60 s209 s207))
(define-fun s212 () (_ BitVec 32) (bvor s210 s211))
(define-fun s213 () (_ BitVec 32) (ite s56 s212 s210))
(define-fun s215 () (_ BitVec 32) (bvor s213 s214))
(define-fun s216 () (_ BitVec 32) (ite s52 s215 s213))
(define-fun s218 () (_ BitVec 32) (bvor s216 s217))
(define-fun s219 () (_ BitVec 32) (ite s48 s218 s216))
(define-fun s221 () (_ BitVec 32) (bvor s219 s220))
(define-fun s222 () (_ BitVec 32) (ite s44 s221 s219))
(define-fun s224 () (_ BitVec 32) (bvor s222 s223))
(define-fun s225 () (_ BitVec 32) (ite s40 s224 s222))
(define-fun s227 () (_ BitVec 32) (bvor s225 s226))
(define-fun s228 () (_ BitVec 32) (ite s36 s227 s225))
(define-fun s230 () (_ BitVec 32) (bvor s228 s229))
(define-fun s231 () (_ BitVec 32) (ite s32 s230 s228))
(define-fun s233 () (_ BitVec 32) (bvor s231 s232))
(define-fun s234 () (_ BitVec 32) (ite s28 s233 s231))
(define-fun s236 () (_ BitVec 32) (bvor s234 s235))
(define-fun s237 () (_ BitVec 32) (ite s24 s236 s234))
(define-fun s238 () (_ BitVec 32) (bvor s13 s237))
(define-fun s239 () (_ BitVec 32) (ite s20 s238 s237))
(define-fun s240 () (_ BitVec 32) (ite s12 s13 s239))
(assert s5)
(assert s6)
(assert s9)
(assert s16)
(assert (= s240 s241))
(minimize s241)
(check-sat)
(get-objectives)
(get-value (s0))
(get-value (s1))
(get-value (s14))
(get-value (s241))
Metadata
Metadata
Assignees
Labels
No labels