Replies: 1 comment 1 reply
-
The description of solver.reset is that it removes all asserted formulas from the solver state. It does not mean the memory is freed because there are structures, such as watch lists and pool allocators that sit around.
|
Beta Was this translation helpful? Give feedback.
-
I wanted to know if there are any descriptions of when max memory exceeded error occurs.
I don't think this is a physical memory limitation.
Context:
I am performing many iterative solver calls. In some procedures, I try to find (binary search) a constant, until solver gives sat or unsat. In other procedures, I perform CEGIS style interactions between 2 solver instances.
In many cases, if I recreate a solver from scratch, for the same set of assertions, the solver now gives a solution instead of memory exceeded.
I am using the python API.
Sample error
Questions:
Thanks!
Beta Was this translation helpful? Give feedback.
All reactions