HOTFIX abort rewrite when SMT solver times out

[jberthold]

When the SMT solver timed out while checking requires clauses of a rule, the unclear conditions were returned in the same way as conditions that were known to be indeterminate. This created bogus branches in proofs when the solver had a problem to decide a condition.

On such timeouts, and on inconsistent ground truths, booster now aborts the entire rewrite. This might lead to increased spurious aborts in complex proofs, but is probably better than having to prune the bogus branches from the client side. The fall-back to legacy kore was able to prune the bogus branch easily in the case that was investigated.

[PetarMax]

If a ground truth is inconsistent, the branch is vacuous, we should return the vacuous result, no?

[jberthold]

KEVM tests

Test	HOTFIX-abort-branching-on-SMT-timeouts time	master-636e1f7f6 time	(HOTFIX-abort-branching-on-SMT-timeouts/master-636e1f7f6) time
examples/sum-to-n-spec.k	88.04	94.35	0.9331213566507686
benchmarks/overflow00-nooverflow-spec.k	46.43	48.2	0.9632780082987551
kontrol/test-allowchangestest-testallow_fail-0-spec.k	48.16	46.53	1.0350311626907371
erc20/hkg/transfer-failure-1-spec.k	58.39	56.35	1.0362023070097603
TOTAL	241.01999999999998	245.43	0.9820315364869819

[jberthold]

If a ground truth is inconsistent, the branch is vacuous, we should return the vacuous result, no?

If the ground truth is inconsistent, the question is how did we even get here?

• if the state got rewritten before, we should have detected it and not rewritten.
• if the state did not get rewritten, the input was already inconsistent. We had an open PR to detect this, I have to check what happened to it. Aborting in booster is a safe option in that case. Tthe inconsistency would also be detected when simplifying the result state....

[jberthold]

Kontrol tests, usual noise (parallelism 4)

Test	HOTFIX-abort-branching-on-SMT-timeouts time	master-636e1f7f6 time	(HOTFIX-abort-branching-on-SMT-timeouts/master-636e1f7f6) time
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_merge_loop_heads	61.69	90.67	0.6803793978162567
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_merge_nodes	5.71	7.43	0.7685060565275909
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_show_with_hex_encoding	5.45	6.92	0.7875722543352601
HevmTests.proveFail_all_branches	36.58	46.13	0.7929763711250812
BytesTypeTest.test_bytes32(bytes32)	12.2	13.77	0.8859840232389252
EmitContractTest.testExpectEmitDoNotCheckData()	15.82	17.84	0.8867713004484306
StoreTest.testStoreLoadNonExistent()	12.91	14.43	0.8946638946638947
BlockParamsTest.testBlockNumber()	11.9	13.3	0.8947368421052632
GasTest.testSetGas()	12.3	13.65	0.9010989010989011
BlockParamsTest.testWarp(uint256)-trace_options2	18.31	19.8	0.9247474747474747
FreshCheatcodes.test_bool()	12.96	13.91	0.9317038102084831
StoreTest.testGasLoadWarmUp()	16.59	17.8	0.9320224719101123
StoreTest.testGasStoreWarmUp()	16.73	17.86	0.9367301231802913
])	29.6	31.51	0.9393843224373215
FreshCheatcodes.test_address()	13.47	14.32	0.9406424581005587
LoopsTest.test_sum_10()	19.74	20.94	0.9426934097421202
CopyStorageTest.testCopyStorage()	36.0	38.09	0.9451299553688631
CoinBaseTest.test_coinbase_setup()	24.48	25.8	0.9488372093023256
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_remove_node	9.19	9.64	0.9533195020746887
MockCallTestFoundry.testRevertMock()	25.23	26.45	0.9538752362948961
MockCallTest.testSelectorMockCall()	25.28	26.48	0.9546827794561934
SymbolicStorageTest.testFail_SymbolicStorage1(uint256)	30.98	32.35	0.9576506955177743
ERC20.sol	50.98	53.0	0.9618867924528302
AllowChangesTest.testFailAllowCallsToAddress()	16.8	16.19	1.0376775787523163
MockCallTestFoundry.testMockSelector()	29.09	27.94	1.0411596277738009
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_xml_report	22.12	21.22	1.0424128180961358
AddrTest.test_addr_true()-trace_options1	30.07	28.67	1.0488315312173002
MockFunctionTest.test_mock_function_all_args()	45.5	43.22	1.052753354928274
FreshCheatcodes.test_freshSymbolicWord()	13.62	12.93	1.0533642691415313
PlainPrankTest.test_startPrank_true()	19.46	18.43	1.0558871405317418
HevmTests.prove_revert	15.7	14.84	1.0579514824797844
FreshCheatcodes.test_int128()	13.76	13.0	1.0584615384615383
],uint256))	28.31	26.64	1.0626876876876876
ChainIdTest.test_chainid_setup()	26.08	24.5	1.0644897959183672
CounterTest.testSetNumber(uint256)	23.08	21.66	1.0655586334256693
StoreTest.testGasLoadColdVM()	15.55	14.52	1.0709366391184574
StoreTest.testGasStoreColdVM()	15.77	14.49	1.088336783988958
StoreTest.testLoadNonExistent()	13.86	12.69	1.0921985815602837
PlainPrankTest.test_startPrankWithOrigin_true()	23.29	21.32	1.0924015009380863
SymbolicStorageTest.testEmptyInitialStorage(uint256)	17.91	16.37	1.0940745265729994
LabelTest.testLabel()	13.4	12.2	1.098360655737705
CounterTest.testIncrement()	21.79	19.74	1.1038500506585613
MethodDisambiguateTest.test_method_call()	13.48	12.2	1.1049180327868853
EmitContractTest.testExpectEmitCheckEmitter()	17.65	15.86	1.1128625472887768
BlockParamsTest.testRoll(uint256)	14.64	13.04	1.1226993865030677
ConstructorTest.run_constructor()	13.46	11.79	1.1416454622561494
BlockParamsTest.testChainId(uint256)	14.98	13.12	1.141768292682927
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_refute_node	51.51	37.16	1.386167922497309
HevmTests.prove_require_assert_false	48.5	34.67	1.3989039515431207
AccountParamsTest.testDealConcrete()-trace_options0	26.85	18.6	1.4435483870967742
TOTAL	1110.33	1109.10	1.0011090073032187