8000 Potential issue in arithmetic optimization · Issue #7677 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Potential issue in arithmetic optimization #7677

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
Open
merlinsun opened this issue Jun 11, 2025 · 2 comments
Open

Potential issue in arithmetic optimization #7677

merlinsun opened this issue Jun 11, 2025 · 2 comments
Labels
Arithmetic bug

Comments

@merlinsun
Copy link

Hi,

I came across a potential correctness issue in the arithmetic optimization when using opt.optsmt_engine=symba. The two following inputs, which appear semantically similar, yield different objective values:

$ z3 opt.optsmt_engine=symba small_int.smt2        
sat
(objectives
 ((- a) oo)
 (a oo)
)
$ cat small_int.smt2
(set-option :opt.priority box)
(declare-const a Int) 
(assert (< 0 (div a 0))) 
(maximize (- a)) 
(maximize a) 
(check-sat) 
(get-objectives) 
$ z3 opt.optsmt_engine=symba small_mix.smt2  
sat
(objectives
 ((- a) 0)
 (a 0)
)
$ cat small_mix.smt2
(set-option :opt.priority box)
(declare-const a Real) 
(assert (< 0 (div (to_int a) 0))) 
(maximize (- a)) 
(maximize a) 
(check-sat) 
(get-objectives)

Commit: 423930d

Additionally, while inspecting, I encountered a possible memory leak:

$ cat leak.smt2
(assert (< 0 (div 0 0)))
(check-sat)
$ z3 leak.smt2
sat

=================================================================
==2329==ERROR: LeakSanitizer: detected memory leaks

Indirect leak of 4268 byte(s) in 1 object(s) allocated from:
    #0 0x7f73aeb56510 in __interceptor_realloc ../../../../src/libsanitizer/asan/asan_malloc_linux.cpp:164
    #1 0x558ac6cf9908 in memory::reallocate(void*, unsigned long) ../src/util/memory_manager.cpp:336
    #2 0x558ac3552c2c in vector<int, false, unsigned int>::expand_vector() ../src/util/vector.h:639
    #3 0x558ac373b963 in void vector<int, false, unsigned int>::resize<int>(unsigned int, int, ...) ../src/util/vector.h:1042
    #4 0x558ac59a6101 in heap<lp::lpvar_lt>::set_bounds(int) ../src/util/heap.h:166
    #5 0x558ac5a7ef6a in heap<lp::lpvar_lt>::heap(int, lp::lpvar_lt const&) ../src/util/heap.h:134
...
SUMMARY: AddressSanitizer: 19512 byte(s) leaked in 151 allocation(s).
@NikolajBjorner
Copy link
Contributor

thanks

@merlinsun
Copy link
Author

Glad it helped!

@github-actions github-actions bot added bug Arithmetic build/release build and release scripts and process performance Issues that relate primarily to the performance of Z3, such as timeouts labels Jun 12, 2025
@NikolajBjorner NikolajBjorner removed build/release build and release scripts and process performance Issues that relate primarily to the performance of Z3, such as timeouts labels Jun 12, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
Arithmetic bug
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@NikolajBjorner @merlinsun
0