8000 Optimization bug, introduced in https://github.com/Z3Prover/z3/commit/fd77f0c1116d0fa0a62a804217137ba15ece8b12 · Issue #5605 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
LeventErkok opened this issue Oct 18, 2021 · 6 comments
Closed

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

LeventErkok opened this issue Oct 18, 2021 · 6 comments

Comments

@LeventErkok
Copy link
LeventErkok commented Oct 18, 2021 •
edited
Loading

@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))
(defi
8000
ne-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
Copy link
Author
LeventErkok commented Oct 18, 2021 •
edited
Loading

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
Copy link
Contributor

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
Copy link
Author

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
Copy link
Author
LeventErkok commented Oct 19, 2021 •
edited
Loading

@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.

@LeventErkok LeventErkok changed the title Floats: Bug with optimization Optimization bug, introduced in https://github.com/Z3Prover/z3/commit/fd77f0c1116d0fa0a62a804217137ba15ece8b12 Oct 19, 2021
NikolajBjorner added a commit that referenced this issue Oct 19, 2021
@NikolajBjorner
#5605
f9dde2e 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
NikolajBjorner added a commit that referenced this issue Oct 19, 2021
@NikolajBjorner
#5605
86147d0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
Copy link
Contributor

I believe the updates now fixed the issue.

@LeventErkok
Copy link
Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@LeventErkok @NikolajBjorner @wintersteiger
0