tests: pass enable_context_search to ContextManager, not ProofController - #15
Open
dingf3ng wants to merge 1 commit into
Open
tests: pass enable_context_search to ContextManager, not ProofController#15dingf3ng wants to merge 1 commit into
dingf3ng wants to merge 1 commit into
Conversation
dingf3ng
force-pushed
the
tests-context-search-kwarg
branch
from
September 2, 2026 07:36
6cb58ee to
5fda0b5
Compare
Three tests passed enable_context_search= to ProofController, which does
not take it -- the flag belongs to ContextManager, which is where main.py
passes it. ProofController takes max_context_search, a different knob.
Every one of them died at construction:
TypeError: ProofController.__init__() got an unexpected keyword
argument 'enable_context_search'
test_folder_batch is the batch runner over AutoRocq-bench, so it could
not prove a single file. test_controller_prove hid it: the exception is
caught, the function returns False, and pytest discards the return, so it
reported a pass while proving nothing.
Moving the flag to the ContextManager call, matching main.py, is enough.
Driving the batch runner over the first five svcomp goals afterwards:
True 16s array_1-2/main_assert_reachability.v
True 59s array_1-2/main_loop_invariant_2_preserved.v
False 80s base_case/main_assert_reachability.v
False 60s benchmark02_linear/..._inv_i_bounds_established.v
True 11s benchmark02_linear/..._inv_i_bounds_preserved.v
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
dingf3ng
force-pushed
the
tests-context-search-kwarg
branch
from
September 2, 2026 07:57
5fda0b5 to
f82ba88
Compare
dingf3ng
changed the base branch from
always-scratch
to
tests-config-fixture
September 2, 2026 07:58
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Why
Three tests pass
enable_context_search=toProofController, which doesn't accept it. The flag belongs toContextManager— which is wheremain.pypasses it.ProofControllertakesmax_context_search, a different knob.All three die at construction:
test_folder_batchis the batch runner over AutoRocq-bench — it could not prove a single file. Andtest_controller_provehid the failure: the exception is caught, the function returnsFalse, and pytest discards the return, so it reported a pass while proving nothing.What changed
Moved the flag to the
ContextManagercall in all three, matchingmain.py. Nothing else.Result
Driving the batch runner over the first five svcomp goals, which previously crashed 5/5: