Merge remote-tracking branch 'origin/develop'

runtimeverification · Aug 8, 2024 · b3637e8 · b3637e8
2 parents 7efd290 + 1e01eea
commit b3637e8
Showing 1 changed file with 11 additions and 6 deletions.
diff --git a/pyk/src/pyk/kore/rpc.py b/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()