Commits on Mar 21, 2024

1. fix(smt-lib): Respect reproducible-resource-limit specification …

   The SMT-LIB standard documentation for the `reproducible-resource-limit`
   option states:
   
   > Setting it a non-zero numeral n will cause each subsequent check
   > command to terminate within a bounded amount of time dependent on n.
   
   We are currently using this as a boolean toggle to switch to the
   "timelimit per goal" interpretation of timeouts, but we are *not*
   respecting the fact that the limit must be dependent on n. Instead, the
   limit must be fixed by the user on the command line; if no timeout is
   passed on the command line, the `reproducible-resource-limit` option
   currently has no effect.
   
   This patch changes it so that setting `reproducible-resource-limit` also
   sets the timeout (expressed in ms), making the behavior compatible with
   the specification.
   
   Note that an unfortunate side-effect is that user-provided timeouts
   passed on the command line are no longer respected, because per-goal and
   global timeouts are mutually exclusive. This is its own issue that
   should be tackled separately if needed.

   

   bclement-ocp committed Mar 21, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for 57b182c
   • Browse repository at this point

   Copy the full SHA

   57b182c View commit details

   Browse the repository at this point in the history