Memory Leak about sat.lookahead.delta_fraction #7372
Description
Hi
Z3 [version 4.13.1 - 64 bit].
ubuntu:22.04
for this case:
(set-logic QF_FPBV)
(declare-fun x () (_ FloatingPoint 11 53))
(declare-fun y () (_ BitVec 64))
(assert (fp.gt x ((_ to_fp 11 53) RNE 1.0)))
(assert (bvult y #x8000000000000000))
(check-sat)
z3 test.smt2
sat
When (set-option:sat.lookahead.delta_fraction 0.3) is added, a memory leak will be triggered
(set-option :sat.lookahead.delta_fraction 0.3)
(set-logic QF_FPBV)
(declare-fun x () (_ FloatingPoint 11 53))
(declare-fun y () (_ BitVec 64))
(assert (fp.gt x ((_ to_fp 11 53) RNE 1.0)))
(assert (bvult y #x8000000000000000))
(check-sat)
z3 test.smt2
unknown
=================================================================
==2725223==ERROR: LeakSanitizer: detected memory leaks
Direct leak of 4408 byte(s) in 1 object(s) allocated from:
#0 0x55d2b09eb36e in malloc (/yuhao/z3/build/z3+0x28436e) (BuildId: 5c00c5286df32e49d27f99f213a657243f3d2f76)
#1 0x55d2b5f0ec95 in memory::allocate(unsigned long) /yuhao/z3/build/../src/util/memory_manager.cpp:301:16
SUMMARY: AddressSanitizer: 4408 byte(s) leaked in 1 allocation(s).
I also found that when the value of the option is set to 0.1/0.2, normal solving will not trigger the vulnerability.