Bug not allowing --smt-retry-limit 0 (#4581)

We were checking `if self.smt_retry_limit` to see if the
`--smt-retry-limit` option should be passed to `kore-rpc-booster`. This
will evaluate to false when it's 0, so the option will not be passed.
However there are cases where we want to pass `--smt-retry-limit 0` to
the kore server. This fixes the check to be `if self.smt_retry_limit is
not None` so it will only not fire if the option is not set. Also fixes
this issue for other KoreServer args.

Also fixes the validation of arguments not being done of the base
`KoreServer` args when using `BoosterServer`. In both cases, changes
`check_if_positive` to `check_if_nonnegative` for `smt_retry_limit` to
allow passing 0.

I confirmed this allows `--smt-retry-limit` to make it through to the
`kore-rpc-booster` command when passed to `kontrol prove`.

---------

Co-authored-by: Petar Maksimović <[email protected]>

pyk/src/pyk/kore/rpc.py

@@ -1227,10 +1227,14 @@ def _check_none_or_positive(n: int | None, param_name: str) -> None:
             if n is not None and n <= 0:
                 raise ValueError(f'Expected positive integer for: {param_name}, got: {n}')
 
+        def _check_none_or_nonnegative(n: int | None, param_name: str) -> None:
+            if n is not None and n < 0:
+                raise ValueError(f'Expected non-negative integer for: {param_name}, got: {n}')
+
         check_dir_path(self._kompiled_dir)
         check_file_path(self._definition_file)
         _check_none_or_positive(self._smt_timeout, 'smt_timeout')
-        _check_none_or_positive(self._smt_retry_limit, 'smt_retry_limit')
+        _check_none_or_nonnegative(self._smt_retry_limit, 'smt_retry_limit')
         _check_none_or_positive(self._smt_reset_interval, 'smt_reset_interval')
 
     def _cli_args(self) -> list[str]:
@@ -1244,16 +1248,16 @@ def _cli_args(self) -> list[str]:
     def _extra_args(self) -> list[str]:
         """Command line arguments that are intended to be included in the bug report."""
         smt_server_args = []
-        if self._smt_timeout:
+        if self._smt_timeout is not None:
             smt_server_args += ['--smt-timeout', str(self._smt_timeout)]
-        if self._smt_retry_limit:
+        if self._smt_retry_limit is not None:
             smt_server_args += ['--smt-retry-limit', str(self._smt_retry_limit)]
-        if self._smt_reset_interval:
+        if self._smt_reset_interval is not None:
             smt_server_args += ['--smt-reset-interval', str(self._smt_reset_interval)]
-        if self._smt_tactic:
+        if self._smt_tactic is not None:
             smt_server_args += ['--smt-tactic', self._smt_tactic]
 
-        if self._log_axioms_file:
+        if self._log_axioms_file is not None:
             haskell_log_args = [
                 '--log',
                 str(self._log_axioms_file),
@@ -1359,6 +1363,7 @@ def _validate(self) -> None:
 
         if self._interim_simplification and self._interim_simplification < 0:
             raise ValueError(f"'interim_simplification' must not be negative, got: {self._interim_simplification}")
+        super()._validate()
 
     def _extra_args(self) -> list[str]:
         res = super()._extra_args()