Optimization bug, introduced in https://github.com/Z3Prover/z3/commit/fd77f0c1116d0fa0a62a804217137ba15ece8b12

[LeventErkok]

@wintersteiger

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))

[LeventErkok]

Here's another example of the same; a bit smaller using smaller sizes for exponent and significand. (Semantically the same as above, just fewer lines.)

(set-option :produce-models true)
(set-logic QF_FPBV)
(define-fun s16 () (_ BitVec 9) #b100000000)
(define-fun s21 () (_ BitVec 1) #b0)
(define-fun s56 () (_ BitVec 9) #b000000001)
(define-fun s57 () (_ BitVec 9) #b000000000)
(define-fun s59 () (_ BitVec 9) #b000000010)
(define-fun s62 () (_ BitVec 9) #b000000100)
(define-fun s65 () (_ BitVec 9) #b000001000)
(define-fun s68 () (_ BitVec 9) #b000010000)
(define-fun s71 () (_ BitVec 9) #b000100000)
(define-fun s74 () (_ BitVec 9) #b001000000)
(define-fun s77 () (_ BitVec 9) #b010000000)
(declare-fun s0 () (_ FloatingPoint 4 5))
(declare-fun s1 () (_ FloatingPoint 4 5))
(declare-fun s17 () (_ BitVec 9)) ; tracks user variable "__internal_sbv_s17"
(declare-fun s83 () (_ BitVec 9)) ; 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 4 5) (fp.add roundNearestTiesToEven s0 s1))
(define-fun s8 () Bool (fp.isNaN s7))
(define-fun s9 () Bool (fp.isInfinite s7))
(define-fun s10 () Bool (or s8 s9))
(define-fun s11 () Bool (not s10))
(define-fun s12 () Bool (not s8))
(define-fun s13 () Bool (fp.isZero s7))
(define-fun s14 () Bool (fp.isNegative s7))
(define-fun s15 () Bool (and s13 s14))
(define-fun s18 () (_ FloatingPoint 4 5) ((_ to_fp 4 5) s17))
(define-fun s19 () Bool (= s7 s18))
(define-fun s20 () (_ BitVec 1) ((_ extract 8 8) s17))
(define-fun s22 () Bool (distinct s20 s21))
(define-fun s23 () Bool (not s22))
(define-fun s24 () (_ BitVec 1) ((_ extract 7 7) s17))
(define-fun s25 () Bool (distinct s21 s24))
(define-fun s26 () Bool (not s25))
(define-fun s27 () Bool (ite s22 s26 s25))
(define-fun s28 () (_ BitVec 1) ((_ extract 6 6) s17))
(define-fun s29 () Bool (distinct s21 s28))
(define-fun s30 () Bool (not s29))
(define-fun s31 () Bool (ite s22 s30 s29))
(define-fun s32 () (_ BitVec 1) ((_ extract 5 5) s17))
(define-fun s33 () Bool (distinct s21 s32))
(define-fun s34 () Bool (not s33))
(define-fun s35 () Bool (ite s22 s34 s33))
(define-fun s36 () (_ BitVec 1) ((_ extract 4 4) s17))
(define-fun s37 () Bool (distinct s21 s36))
(define-fun s38 () Bool (not s37))
(define-fun s39 () Bool (ite s22 s38 s37))
(define-fun s40 () (_ BitVec 1) ((_ extract 3 3) s17))
(define-fun s41 () Bool (distinct s21 s40))
(define-fun s42 () Bool (not s41))
(define-fun s43 () Bool (ite s22 s42 s41))
(define-fun s44 () (_ BitVec 1) ((_ extract 2 2) s17))
(define-fun s45 () Bool (distinct s21 s44))
(define-fun s46 () Bool (not s45))
(define-fun s47 () Bool (ite s22 s46 s45))
(define-fun s48 () (_ BitVec 1) ((_ extract 1 1) s17))
(define-fun s49 () Bool (distinct s21 s48))
(define-fun s50 () Bool (not s49))
(define-fun s51 () Bool (ite s22 s50 s49))
(define-fun s52 () (_ BitVec 1) ((_ extract 0 0) s17))
(define-fun s53 () Bool (distinct s21 s52))
(define-fun s54 () Bool (not s53))
(define-fun s55 () Bool (ite s22 s54 s53))
(define-fun s58 () (_ BitVec 9) (ite s55 s56 s57))
(define-fun s60 () (_ BitVec 9) (bvor s58 s59))
(define-fun s61 () (_ BitVec 9) (ite s51 s60 s58))
(define-fun s63 () (_ BitVec 9) (bvor s61 s62))
(define-fun s64 () (_ BitVec 9) (ite s47 s63 s61))
(define-fun s66 () (_ BitVec 9) (bvor s64 s65))
(define-fun s67 () (_ BitVec 9) (ite s43 s66 s64))
(define-fun s69 () (_ BitVec 9) (bvor s67 s68))
(define-fun s70 () (_ BitVec 9) (ite s39 s69 s67))
(define-fun s72 () (_ BitVec 9) (bvor s70 s71))
(define-fun s73 () (_ BitVec 9) (ite s35 s72 s70))
(define-fun s75 () (_ BitVec 9) (bvor s73 s74))
(define-fun s76 () (_ BitVec 9) (ite s31 s75 s73))
(define-fun s78 () (_ BitVec 9) (bvor s76 s77))
(define-fun s79 () (_ BitVec 9) (ite s27 s78 s76))
(define-fun s80 () (_ BitVec 9) (bvor s16 s79))
(define-fun s81 () (_ BitVec 9) (ite s23 s80 s79))
(define-fun s82 () (_ BitVec 9) (ite s15 s16 s81))
(assert s5)
(assert s6)
(assert s11)
(assert s12)
(assert s19)
(assert (= s82 s83))
(minimize s83)
(check-sat)
(get-objectives)
(get-value (s7))
(get-value (s0))
(get-value (s1))
(get-value (s17))
(get-value (s83))

Correct answer, obtained by August 17, 2021 z3:

sat
(objectives
 (s83 16)
)
((s7 (fp #b1 #xe #xf)))
((s0 (fp #b1 #xd #xf)))
((s1 (fp #b1 #xd #xf)))
((s17 #b111101111))
((s83 #b000010000))

Incorrect answer, produced by current master z3:

sat
(objectives
 (s83 2)
)
((s7 (fp #b0 #x0 #x2)))
((s0 (fp #b0 #x0 #x1)))
((s1 (fp #b0 #x0 #x1)))
((s17 #b000000010))
((s83 #b100000010))

[wintersteiger]

This one will be very hard to debug. There are bugs in the optimization engine, which I am not even a little bit familiar with, so if this still fails after the other FP bugs are fixed, I'll have to ask @NikolajBjorner to take a look at this. In any case, this will take a very long time to resolve.

[LeventErkok]

Thanks @wintersteiger

I've a feeling this doesn't have anything to do with the optimizer, but just manifests that way; but it could also be a weird interaction indeed. I'll see if I can do some git-bisecting to at least determine which exact commit broke it. Perhaps that'll provide some more incentive/guidance as to what the real culprit might be.

[LeventErkok]

@wintersteiger @NikolajBjorner

After git-bisecting, I found that the following commit (by Nikolaj) is the culprit for this bug:

fd77f0c

And just by looking at the commit itself, looks like this really doesn't have anything to do with floats at all. I can't tell from the changes why, but this is the commit that broke this benchmark.

[NikolajBjorner]

I believe the updates now fixed the issue.

[LeventErkok]

Yes! I can confirm that the benchmark now works as expected. Thanks for the quick fix.