From 755f3f2d5469c01c7ad4a37be770749ad12db419 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Thu, 10 Oct 2024 16:07:44 -0700 Subject: [PATCH] fix: reset z3 solver objects (#389) --- .github/workflows/test-external.yml | 2 +- .github/workflows/test.yml | 4 +- requirements-dev.txt | 1 - src/halmos/__main__.py | 204 +++++++++------------------- src/halmos/calldata.py | 6 +- src/halmos/cheatcodes.py | 9 +- src/halmos/config.py | 16 ++- src/halmos/sevm.py | 23 +++- src/halmos/utils.py | 8 +- tests/regression/halmos.toml | 6 +- 10 files changed, 111 insertions(+), 168 deletions(-) diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml index 3681330f..d454c8fb 100644 --- a/.github/workflows/test-external.yml +++ b/.github/workflows/test-external.yml @@ -92,7 +92,7 @@ jobs: - name: Install Vyper if: ${{ matrix.project.dir == 'snekmate' }} run: | - docker run --name halmos-vyper --entrypoint uv halmos-image pip install vyper + docker run --name halmos-vyper --entrypoint uv halmos-image pip install git+https://github.com/vyperlang/vyper@master docker commit --change 'ENTRYPOINT ["halmos"]' halmos-vyper halmos-image - name: Checkout external repo diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 48e38374..05114503 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -27,7 +27,6 @@ jobs: matrix: os: ["macos-latest", "ubuntu-latest", "windows-latest"] python-version: ["3.11", "3.12"] - parallel: ["", "--test-parallel"] storage-layout: ["solidity", "generic"] cache-solver: ["", "--cache-solver"] @@ -35,6 +34,7 @@ jobs: - name: Checkout repository uses: actions/checkout@v4 with: + # note: it is faster to let foundry do a sparse checkout of the missing libraries rather than having the action do a git checkout of the submodules submodules: false - name: Install foundry @@ -54,4 +54,4 @@ jobs: run: python -m pip install -e . - name: Run pytest - run: pytest -v -k "not long and not ffi" --ignore=tests/lib --halmos-options="-st ${{ matrix.parallel }} --solver-threads 1 --storage-layout ${{ matrix.storage-layout }} ${{ matrix.cache-solver }} --solver-timeout-assertion 0 ${{ inputs.halmos-options }}" ${{ inputs.pytest-options }} + run: pytest -v -k "not long and not ffi" --ignore=tests/lib --halmos-options="-st --disable-gc --solver-threads 1 --storage-layout ${{ matrix.storage-layout }} ${{ matrix.cache-solver }} --solver-timeout-assertion 0 ${{ inputs.halmos-options }}" ${{ inputs.pytest-options }} diff --git a/requirements-dev.txt b/requirements-dev.txt index 86a3d234..30544ac2 100644 --- a/requirements-dev.txt +++ b/requirements-dev.txt @@ -1,4 +1,3 @@ black pre-commit pytest -pytest-xdist diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 367adeb6..47e16a9e 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -1,5 +1,6 @@ # SPDX-License-Identifier: AGPL-3.0 +import gc import io import json import os @@ -11,7 +12,7 @@ import traceback import uuid from collections import Counter -from concurrent.futures import ProcessPoolExecutor, ThreadPoolExecutor +from concurrent.futures import ThreadPoolExecutor from copy import deepcopy from dataclasses import asdict, dataclass from enum import Enum @@ -26,6 +27,7 @@ CheckSatResult, Context, ModelRef, + Solver, is_app, is_bv, sat, @@ -95,7 +97,7 @@ ) StrModel = dict[str, str] -AnyModel = ModelRef | StrModel +AnyModel = StrModel | str # Python version >=3.8.14, >=3.9.14, >=3.10.7, or >=3.11 if hasattr(sys, "set_int_max_str_digits"): @@ -339,6 +341,7 @@ def deploy_test( sevm: SEVM, args: HalmosConfig, libs: dict, + solver: Solver, ) -> Exec: this = mk_this() message = Message( @@ -357,7 +360,7 @@ def deploy_test( block=mk_block(), context=CallContext(message=message), pgm=None, # to be added - path=Path(mk_solver(args)), + path=Path(solver), ) # deploy libraries and resolve library placeholders in hexcode @@ -409,12 +412,13 @@ def setup( setup_info: FunctionInfo, args: HalmosConfig, libs: dict, + solver: Solver, ) -> Exec: setup_timer = NamedTimer("setup") setup_timer.create_subtimer("decode") sevm = SEVM(args) - setup_ex = deploy_test(creation_hexcode, deployed_hexcode, sevm, args, libs) + setup_ex = deploy_test(creation_hexcode, deployed_hexcode, sevm, args, libs, solver) setup_timer.create_subtimer("run") @@ -504,11 +508,33 @@ def setup( return setup_ex +@dataclass +class PotentialModel: + model: AnyModel + is_valid: bool + + def __init__(self, model: ModelRef | str, args: HalmosConfig) -> None: + # convert model into string to avoid pickling errors for z3 (ctypes) objects containing pointers + self.model = ( + to_str_model(model, args.print_full_model) + if isinstance(model, ModelRef) + else model + ) + self.is_valid = is_model_valid(model) + + def __str__(self) -> str: + # expected to be a filename + if isinstance(self.model, str): + return f"see {self.model}" + + formatted = [f"\n {decl} = {val}" for decl, val in self.model.items()] + return "".join(sorted(formatted)) if formatted else "∅" + + @dataclass(frozen=True) class ModelWithContext: # can be a filename containing the model or a dict with variable assignments - model: StrModel | str | None - is_valid: bool | None + model: PotentialModel | None index: int result: CheckSatResult unsat_core: list | None @@ -544,6 +570,7 @@ def run( abi: dict, fun_info: FunctionInfo, args: HalmosConfig, + solver: Solver, ) -> TestResult: funname, funsig = fun_info.name, fun_info.sig if args.verbose >= 1: @@ -556,7 +583,6 @@ def run( # sevm = SEVM(args) - solver = mk_solver(args) path = Path(solver) path.extend_path(setup_ex.path) @@ -623,7 +649,7 @@ def future_callback(future_model): m = future_model.result() models.append(m) - model, is_valid, index, result = m.model, m.is_valid, m.index, m.result + model, index, result = m.model, m.index, m.result if result == unsat: if m.unsat_core: unsat_cores.append(m.unsat_core) @@ -631,13 +657,13 @@ def future_callback(future_model): # model could be an empty dict here if model is not None: - if is_valid: - print(red(f"Counterexample: {render_model(model)}")) + if model.is_valid: + print(red(f"Counterexample: {model}")) counterexamples.append(model) else: warn_code( COUNTEREXAMPLE_INVALID, - f"Counterexample (potentially invalid): {render_model(model)}", + f"Counterexample (potentially invalid): {model}", ) counterexamples.append(model) else: @@ -787,56 +813,6 @@ def future_callback(future_model): ) -@dataclass(frozen=True) -class SetupAndRunSingleArgs: - creation_hexcode: str - deployed_hexcode: str - abi: dict - setup_info: FunctionInfo - fun_info: FunctionInfo - setup_args: HalmosConfig - args: HalmosConfig - libs: dict - build_out_map: dict - - -def setup_and_run_single(fn_args: SetupAndRunSingleArgs) -> list[TestResult]: - BuildOut().set_build_out(fn_args.build_out_map) - - args = fn_args.args - try: - setup_ex = setup( - fn_args.creation_hexcode, - fn_args.deployed_hexcode, - fn_args.abi, - fn_args.setup_info, - fn_args.setup_args, - fn_args.libs, - ) - except Exception as err: - error(f"Error: {fn_args.setup_info.sig} failed: {type(err).__name__}: {err}") - - if args.debug: - traceback.print_exc() - return [] - - try: - test_result = run( - setup_ex, - fn_args.abi, - fn_args.fun_info, - fn_args.args, - ) - except Exception as err: - print(f"{color_error('[ERROR]')} {fn_args.fun_info.sig}") - error(f"{type(err).__name__}: {err}") - if args.debug: - traceback.print_exc() - return [TestResult(fn_args.fun_info.sig, Exitcode.EXCEPTION.value)] - - return [test_result] - - def extract_setup(methodIdentifiers: dict[str, str]) -> FunctionInfo: setup_sigs = sorted( [ @@ -873,46 +849,6 @@ class RunArgs: build_out_map: dict -def run_parallel(run_args: RunArgs) -> list[TestResult]: - args = run_args.args - creation_hexcode, deployed_hexcode, abi, methodIdentifiers, libs = ( - run_args.creation_hexcode, - run_args.deployed_hexcode, - run_args.abi, - run_args.methodIdentifiers, - run_args.libs, - ) - - setup_info = extract_setup(methodIdentifiers) - setup_config = with_devdoc(args, setup_info.sig, run_args.contract_json) - fun_infos = [ - FunctionInfo(funsig.split("(")[0], funsig, methodIdentifiers[funsig]) - for funsig in run_args.funsigs - ] - - single_run_args = [ - SetupAndRunSingleArgs( - creation_hexcode, - deployed_hexcode, - abi, - setup_info, - fun_info, - setup_config, - with_devdoc(args, fun_info.sig, run_args.contract_json), - libs, - run_args.build_out_map, - ) - for fun_info in fun_infos - ] - - # dispatch to the shared process pool - with ProcessPoolExecutor() as process_pool: - test_results = list(process_pool.map(setup_and_run_single, single_run_args)) - test_results = sum(test_results, []) # flatten lists - - return test_results - - def run_sequential(run_args: RunArgs) -> list[TestResult]: BuildOut().set_build_out(run_args.build_out_map) @@ -921,6 +857,7 @@ def run_sequential(run_args: RunArgs) -> list[TestResult]: try: setup_config = with_devdoc(args, setup_info.sig, run_args.contract_json) + setup_solver = mk_solver(setup_config) setup_ex = setup( run_args.creation_hexcode, run_args.deployed_hexcode, @@ -928,11 +865,14 @@ def run_sequential(run_args: RunArgs) -> list[TestResult]: setup_info, setup_config, run_args.libs, + setup_solver, ) except Exception as err: error(f"Error: {setup_info.sig} failed: {type(err).__name__}: {err}") if args.debug: traceback.print_exc() + # reset any remaining solver states from the default context + setup_solver.reset() return [] test_results = [] @@ -942,9 +882,10 @@ def run_sequential(run_args: RunArgs) -> list[TestResult]: ) try: test_config = with_devdoc(args, funsig, run_args.contract_json) + solver = mk_solver(test_config) if test_config.debug: debug(f"{test_config.formatted_layers()}") - test_result = run(setup_ex, run_args.abi, fun_info, test_config) + test_result = run(setup_ex, run_args.abi, fun_info, test_config, solver) except Exception as err: print(f"{color_error('[ERROR]')} {funsig}") error(f"{type(err).__name__}: {err}") @@ -952,9 +893,15 @@ def run_sequential(run_args: RunArgs) -> list[TestResult]: traceback.print_exc() test_results.append(TestResult(funsig, Exitcode.EXCEPTION.value)) continue + finally: + # reset any remaining solver states from the default context + solver.reset() test_results.append(test_result) + # reset any remaining solver states from the default context + setup_solver.reset() + return test_results @@ -967,10 +914,6 @@ class GenModelArgs: dump_dirname: str | None = None -def copy_model(model: ModelRef) -> dict: - return {decl: model[decl] for decl in model} - - def parse_unsat_core(output) -> list | None: # parsing example: # unsat @@ -990,7 +933,7 @@ def parse_unsat_core(output) -> list | None: def solve( query: SMTQuery, args: HalmosConfig, dump_filename: str | None = None -) -> tuple[CheckSatResult, ModelRef, list | None]: +) -> tuple[CheckSatResult, PotentialModel | None, list | None]: if args.dump_smt_queries or args.solver_command: if not dump_filename: dump_filename = f"/tmp/{uuid.uuid4().hex}.smt2" @@ -1048,7 +991,7 @@ def solve( unsat_core = parse_unsat_core(res_str) if args.cache_solver else None return unsat, None, unsat_core elif res_str_head == "sat": - return sat, f"{dump_filename}.out", None + return sat, PotentialModel(f"{dump_filename}.out", args), None else: return unknown, None, None except subprocess.TimeoutExpired: @@ -1064,12 +1007,13 @@ def solve( result = solver.check(*ids) else: result = solver.check() - model = copy_model(solver.model()) if result == sat else None + model = PotentialModel(solver.model(), args) if result == sat else None unsat_core = ( [str(core) for core in solver.unsat_core()] if args.cache_solver and result == unsat else None ) + solver.reset() return result, model, unsat_core @@ -1102,7 +1046,7 @@ def gen_model_from_sexpr(fn_args: GenModelArgs) -> ModelWithContext: res, model, unsat_core = solve(sexpr, args, dump_filename) - if res == sat and not is_model_valid(model): + if res == sat and not model.is_valid: if args.verbose >= 1: print(" Checking again with refinement") @@ -1112,10 +1056,6 @@ def gen_model_from_sexpr(fn_args: GenModelArgs) -> ModelWithContext: return package_result(model, idx, res, unsat_core, args) -def is_unknown(result: CheckSatResult, model: ModelRef) -> bool: - return result == unknown or (result == sat and not is_model_valid(model)) - - def refine(query: SMTQuery) -> SMTQuery: smtlib = query.smtlib @@ -1139,7 +1079,7 @@ def refine(query: SMTQuery) -> SMTQuery: def package_result( - model: ModelRef | str | None, + model: PotentialModel | None, idx: int, result: CheckSatResult, unsat_core: list | None, @@ -1148,31 +1088,20 @@ def package_result( if result == unsat: if args.verbose >= 1: print(f" Invalid path; ignored (path id: {idx+1})") - return ModelWithContext(None, None, idx, result, unsat_core) + return ModelWithContext(None, idx, result, unsat_core) if result == sat: if args.verbose >= 1: print(f" Valid path; counterexample generated (path id: {idx+1})") - - # convert model into string to avoid pickling errors for z3 (ctypes) objects containing pointers - is_valid = None - if model: - if isinstance(model, str): - is_valid = True - model = f"see {model}" - else: - is_valid = is_model_valid(model) - model = to_str_model(model, args.print_full_model) - - return ModelWithContext(model, is_valid, idx, result, None) + return ModelWithContext(model, idx, result, None) else: if args.verbose >= 1: print(f" Timeout (path id: {idx+1})") - return ModelWithContext(None, None, idx, result, None) + return ModelWithContext(None, idx, result, None) -def is_model_valid(model: AnyModel) -> bool: +def is_model_valid(model: ModelRef | str) -> bool: # TODO: evaluate the path condition against the given model after excluding f_evm_* symbols, # since the f_evm_* symbols may still appear in valid models. @@ -1198,14 +1127,6 @@ def select(var): return {str(decl): stringify(str(decl), model[decl]) for decl in select_model} -def render_model(model: StrModel | str) -> str: - if isinstance(model, str): - return model - - formatted = [f"\n {decl} = {val}" for decl, val in model.items()] - return "".join(sorted(formatted)) if formatted else "∅" - - def get_contract_type( ast_nodes: list, contract_name: str ) -> tuple[str | None, str | None]: @@ -1417,6 +1338,9 @@ def _main(_args=None) -> MainResult: print(f"halmos {metadata.version('halmos')}") return MainResult(0) + if args.disable_gc: + gc.disable() + # # compile # @@ -1530,9 +1454,7 @@ def on_signal(signum, frame): build_out_map, ) - enable_parallel = args.test_parallel and num_found > 1 - run_method = run_parallel if enable_parallel else run_sequential - test_results = run_method(run_args) + test_results = run_sequential(run_args) num_passed = sum(r.exitcode == 0 for r in test_results) num_failed = num_found - num_passed diff --git a/src/halmos/calldata.py b/src/halmos/calldata.py index bb3b1c63..117c64c7 100644 --- a/src/halmos/calldata.py +++ b/src/halmos/calldata.py @@ -12,7 +12,7 @@ from .bytevec import ByteVec from .config import Config as HalmosConfig -from .utils import con +from .utils import con, uid @dataclass(frozen=True) @@ -144,7 +144,7 @@ def get_dyn_sizes(self, name: str, typ: Type) -> tuple[list[int], BitVecRef]: f"Warning: no size provided for {name}; default value {sizes} will be used." ) - size_var = BitVec(f"p_{name}_length_{self.new_symbol_id():>02}", 256) + size_var = BitVec(f"p_{name}_length_{uid()}_{self.new_symbol_id():>02}", 256) self.dyn_params.append(DynamicParam(name, sizes, size_var, typ)) @@ -222,7 +222,7 @@ def encode(self, name: str, typ: Type) -> EncodingResult: return EncodingResult([size_var] + encoded.data, 32 + encoded.size, False) if isinstance(typ, BaseType): - new_symbol = f"p_{name}_{typ.typ}_{self.new_symbol_id():>02}" + new_symbol = f"p_{name}_{typ.typ}_{uid()}_{self.new_symbol_id():>02}" # bytes, string if typ.typ in ["bytes", "string"]: diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index 660ed371..be2e3eb0 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -55,6 +55,7 @@ red, secp256k1n, stripped, + uid, uint160, uint256, ) @@ -292,10 +293,12 @@ def create_calldata_generic(ex, sevm, contract_name, filename=None, include_view results.append(encode_tuple_bytes(b"")) # nonempty calldata for fallback() - fallback_selector = BitVec(f"fallback_selector_{ex.new_symbol_id():>02}", 4 * 8) + fallback_selector = BitVec( + f"fallback_selector_{uid()}_{ex.new_symbol_id():>02}", 4 * 8 + ) fallback_input_length = 1024 # TODO: configurable fallback_input = BitVec( - f"fallback_input_{ex.new_symbol_id():>02}", fallback_input_length * 8 + f"fallback_input_{uid()}_{ex.new_symbol_id():>02}", fallback_input_length * 8 ) results.append(encode_tuple_bytes(Concat(fallback_selector, fallback_input))) @@ -328,7 +331,7 @@ def create_calldata_generic(ex, sevm, contract_name, filename=None, include_view def create_generic(ex, bits: int, var_name: str, type_name: str) -> BitVecRef: - label = f"halmos_{var_name}_{type_name}_{ex.new_symbol_id():>02}" + label = f"halmos_{var_name}_{type_name}_{uid()}_{ex.new_symbol_id():>02}" return BitVec(label, BitVecSorts[bits]) diff --git a/src/halmos/config.py b/src/halmos/config.py index 3664eaa7..6d4a796a 100644 --- a/src/halmos/config.py +++ b/src/halmos/config.py @@ -382,6 +382,12 @@ class Config: group=debugging, ) + disable_gc: bool = arg( + help="disable Python's automatic garbage collection for cyclic objects. This does not affect reference counting based garbage collection.", + global_default=False, + group=debugging, + ) + ### Build options forge_build_out: str = arg( @@ -442,10 +448,6 @@ class Config: ### Experimental options - test_parallel: bool = arg( - help="run tests in parallel", global_default=False, group=experimental - ) - symbolic_jump: bool = arg( help="support symbolic jump destination", global_default=False, @@ -454,6 +456,12 @@ class Config: ### Deprecated + test_parallel: bool = arg( + help="(Deprecated; no-op) run tests in parallel", + global_default=False, + group=deprecated, + ) + solver_parallel: bool = arg( help="(Deprecated; no-op; use --solver-threads instead) run assertion solvers in parallel", global_default=False, diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 76598200..f62053a5 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -26,6 +26,7 @@ BoolVal, CheckSatResult, Concat, + Context, Extract, Function, If, @@ -35,7 +36,6 @@ Select, SignExt, Solver, - SolverFor, SRem, Store, UDiv, @@ -92,6 +92,7 @@ con, con_addr, concat, + create_solver, debug, extract_bytes, f_ecrecover, @@ -112,6 +113,7 @@ sha3_inv, str_opcode, stripped, + uid, uint8, uint160, uint256, @@ -733,10 +735,14 @@ def to_smt2(self, args) -> SMTQuery: ids = [str(cond.get_id()) for cond in self.conditions] if args.cache_solver: - tmp_solver = SolverFor("QF_AUFBV") + # TODO: investigate whether a separate context is necessary here + tmp_solver = create_solver(ctx=Context()) for cond in self.conditions: - tmp_solver.assert_and_track(cond, str(cond.get_id())) + tmp_solver.assert_and_track( + cond.translate(tmp_solver.ctx), str(cond.get_id()) + ) query = tmp_solver.to_smt2() + tmp_solver.reset() else: query = self.solver.to_smt2() query = query.replace("(check-sat)", "") # see __main__.solve() @@ -1090,7 +1096,7 @@ def balance_update(self, addr: Word, value: Word) -> None: assert_uint256(value) addr = uint160(addr) new_balance_var = Array( - f"balance_{1+len(self.balances):>02}", BitVecSort160, BitVecSort256 + f"balance_{uid()}_{1+len(self.balances):>02}", BitVecSort160, BitVecSort256 ) new_balance = Store(self.balance, addr, value) self.path.append(new_balance_var == new_balance) @@ -1236,6 +1242,7 @@ def empty(cls, addr: BitVecRef, slot: int, keys: tuple) -> ArrayRef: num_keys = len(keys) size_keys = cls.bitsize(keys) return Array( + # note: uuid is excluded to be deterministic f"storage_{id_str(addr)}_{slot}_{num_keys}_{size_keys}_00", BitVecSorts[size_keys], BitVecSort256, @@ -1267,6 +1274,7 @@ def init( # size_keys == 0 mapping[size_keys] = ( BitVec( + # note: uuid is excluded to be deterministic f"storage_{id_str(addr)}_{slot}_{num_keys}_{size_keys}_00", BitVecSort256, ) @@ -1310,7 +1318,7 @@ def store(cls, ex: Exec, addr: Any, loc: Any, val: Any) -> None: return new_storage_var = Array( - f"storage_{id_str(addr)}_{slot}_{num_keys}_{size_keys}_{1+len(ex.storages):>02}", + f"storage_{id_str(addr)}_{slot}_{num_keys}_{size_keys}_{uid()}_{1+len(ex.storages):>02}", BitVecSorts[size_keys], BitVecSort256, ) @@ -1405,6 +1413,7 @@ def mk_storagedata(cls) -> StorageData: @classmethod def empty(cls, addr: BitVecRef, loc: BitVecRef) -> ArrayRef: return Array( + # note: uuid is excluded to be deterministic f"storage_{id_str(addr)}_{loc.size()}_00", BitVecSorts[loc.size()], BitVecSort256, @@ -1453,7 +1462,7 @@ def store(cls, ex: Exec, addr: Any, loc: Any, val: Any) -> None: mapping = ex.storage[addr].mapping new_storage_var = Array( - f"storage_{id_str(addr)}_{size_keys}_{1+len(ex.storages):>02}", + f"storage_{id_str(addr)}_{size_keys}_{uid()}_{1+len(ex.storages):>02}", BitVecSorts[size_keys], BitVecSort256, ) @@ -2156,7 +2165,7 @@ def call_unknown() -> None: # push exit code exit_code_var = BitVec( - f"call_exit_code_{ex.new_call_id():>02}", BitVecSort256 + f"call_exit_code_{uid()}_{ex.new_call_id():>02}", BitVecSort256 ) ex.path.append(exit_code_var == exit_code) ex.st.push(exit_code if is_bv_value(exit_code) else exit_code_var) diff --git a/src/halmos/utils.py b/src/halmos/utils.py index 05a13f7f..20f2a1ef 100644 --- a/src/halmos/utils.py +++ b/src/halmos/utils.py @@ -2,6 +2,7 @@ import math import re +import uuid from functools import partial from timeit import default_timer as timer from typing import Any @@ -110,6 +111,10 @@ def f_sha3_name(bitsize: int) -> str: f_sha3_512_name = f_sha3_name(512) +def uid() -> str: + return uuid.uuid4().hex[:7] + + def wrap(x: Any) -> Word: if is_bv(x): return x @@ -221,9 +226,6 @@ def create_solver(logic="QF_AUFBV", ctx=None, timeout=0, max_memory=0): # QF_AUFBV: quantifier-free bitvector + array theory: https://smtlib.cs.uiowa.edu/logics.shtml solver = SolverFor(logic, ctx=ctx) - # reset any remaining solver states from the default context - solver.reset() - # set timeout solver.set(timeout=timeout) diff --git a/tests/regression/halmos.toml b/tests/regression/halmos.toml index a03c9f4d..84710613 100644 --- a/tests/regression/halmos.toml +++ b/tests/regression/halmos.toml @@ -80,6 +80,9 @@ print-mem = false # print all final execution states print-states = false +# print successful execution states +print-success-states = false + # print failed execution states print-failed-states = false @@ -134,8 +137,5 @@ cache-solver = false # Experimental options # ################################################################################ -# run tests in parallel -test-parallel = false - # support symbolic jump destination symbolic-jump = false