search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.42k stars 1.47k forks source link

Complex Memory Leak in Theory of FP with Multiple check-sat Commands #643

Closed kyledewey closed 8 years ago

kyledewey commented 8 years ago

On the master branch at commit bd187e098988c57b5dc8e75480c42717ffeb3482, consider the following input:

(set-logic QF_FP)
(declare-fun x0 () (_ FloatingPoint 2 3))
(check-sat)
(assert (= (fp.isSubnormal (fp.sqrt RTP (fp.max (fp.sqrt RNE (fp.sqrt RTZ (fp.neg (fp.add RTP x0 (fp.neg (fp.abs (fp.mul RTP x0 x0))))))) x0))) true))
(check-sat)
(check-sat)

Placing this into a file test.smtlib2 and running with command-line z3 -smt2 test.smtlib2 yields the following output:

sat
sat
sat
ast_manager LEAKED: 3
Leaked: decl z3.sk.0 :: bv[1]
id: 2147484139
Leaked: decl z3.sk.1 :: bv[1]
id: 2147484140
Leaked: bv

All the (check-sat) commands are necessary. For as large as this input is, this is actually post-minimization with an experimental delta debugger. If this can be further minimized, let me know.

NikolajBjorner commented 8 years ago

Thanks