search

cvc5 / cvc5

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.
Other
1.04k stars 234 forks source link

cvc5 1.1.0 rlimit consumption #10312

Open kanigsson opened 9 months ago

kanigsson commented 9 months ago

repr.smt2.txt

On the attached file, cvc5 seems to not properly respect the rlimit after the first (get-model) (the file contains two calls to get-model).

$ time --rlimit=10000 repr.smt2 sat

unknown user 0m0.218s With rlimit set to 100000, it takes over a minute, and over 4 minutes set to 150000. Likely some code doesn't properly consume resources? **Command line arguments**: `--rlimit` **cvc5 version/commit**: 1.1.0 **Operating system**: Linux, OpenSuse Leap 15.5
netolcc06 commented 8 months ago

Hi @kanigsson,

We are currently revisiting cvc5's resource spending monitoring (especially if at some points we are not spending resources as we should or if the application does not terminate when the limit is reached). I will bring you updates once this analysis is complete.