Skip to content
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.

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

UFs + FPA -> internalizer doesn't respect memory limit #5986

Closed
nunoplopes opened this issue Apr 18, 2022 · 1 comment
Closed

UFs + FPA -> internalizer doesn't respect memory limit #5986

nunoplopes opened this issue Apr 18, 2022 · 1 comment

Comments

@nunoplopes
Copy link
Collaborator

Z3 ignores the memory limit for the attached file. I had to kill it after 8 GBs of memory usage, while the limit is only 2 GBs.

$ z3 memory_high_watermark=2147483648 crash.smt2

The trace is super deep and it's all about the internalizer (is it going on an infinite loop?):

#192 smt::context::internalize_ite_term(app*)
#193 smt::context::internalize_ite_term(app*)
#194 smt::context::internalize_formula_core(app*, bool)
#195 smt::context::internalize_eq(app*, bool)
#196 smt::context::internalize_formula_core(app*, bool)
#197 smt::context::internalize_formula_core(app*, bool)
#198 smt::theory_fpa::assert_cnstr(expr*)
#199 smt::theory_fpa::internalize_atom(app*, bool)
#200 smt::context::internalize_theory_atom(app*, bool)
#201 smt::context::internalize_formula(expr*, bool)
#202 smt::context::assert_default(expr*, app*)
#203 smt::context::internalize_assertion(expr*, app*, unsigned int)
#204 smt::context::internalize_assertions()
#205 smt::context::setup_and_check(bool)

(Upstream report: AliveToolkit/alive2#785)

NikolajBjorner added a commit that referenced this issue Apr 19, 2022
add memory limit check to internalize
@nunoplopes
Copy link
Collaborator Author

Seems fixed, thank you!
Benchmarking it now to check if it regresses smth.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant