Filter SMT lemmas for predicate checks and get-model

[jberthold]

Related: #4034

Booster SMT bindings change as follows:

• SMT lemmas are held in a lookup table separate from the sort and function declarations
• The lookup is by SymbolName, and returns lemmas that (transitively) may relate to the given symbol
• When checking predicates or computing a model, only those lemmas are added which relate to a symbol used in one of the predicates

This is hopefully reducing load on the SMT solver to enable solving problems that came up in engagement proofs and led to timeouts.

[jberthold]

evm-semantics tests with a regression in sum-to-n-spec.k

Test	4043-filter-smt-lemmas-for-predicate-checks time	master-960328a51 time	(4043-filter-smt-lemmas-for-predicate-checks/master-960328a51) time
examples/sum-to-n-spec.k	96.15	70.09	1.3718076758453417
TOTAL	96.15	70.09	1.3718076758453417

[jberthold]

More mixed results for kontrol

Test	4043-filter-smt-lemmas-for-predicate-checks time	master-960328a51 time	(4043-filter-smt-lemmas-for-predicate-checks/master-960328a51) time
SymbolicStorageTest.testEmptyInitialStorage(uint256)	17.6	24.51	0.7180742554059568
ExpectRevertTest.testFail_expectRevert_empty()	12.13	14.59	0.8313913639479096
HevmTests.prove_require_assert_false	37.61	44.7	0.841387024608501
ExpectCallTest.testExpectStaticCall()	17.01	19.32	0.8804347826086957
EmitContractTest.testExpectEmitDoNotCheckData()	15.25	17.28	0.8825231481481481
ExpectRevertTest.test_expectRevert_returnValue()	20.35	22.85	0.8905908096280087
StoreTest.testStoreLoadNonExistent()	12.26	13.76	0.8909883720930233
FeeTest.test_fee_setup()	25.83	28.66	0.9012561060711792
AssertTest.prove_assert_true()	14.25	15.31	0.9307642064010451
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_show_with_hex_encoding	4.5	4.82	0.933609958506224
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_auto_abstraction	29.57	31.13	0.9498875682621266
SetUpDeployTest.test_extcodesize()	42.23	44.14	0.956728590847304
UintTypeTest.test_uint256(uint256)	15.62	15.04	1.038563829787234
])	31.15	29.95	1.0400667779632722
AssertTest.test_assert_true_branch(uint256)	28.56	27.4	1.0423357664233577
Setup2Test.testFail_setup()	30.51	28.44	1.0727848101265822
kontrol/src/tests/integration/test_foundry_prove.py::test_constructor_with_symbolic_args	82.98	76.6	1.0832898172323762
ExpectCallTest.testExpectRegularCall()	18.93	17.12	1.1057242990654206
EmitContractTest.testExpectEmitCheckEmitter()	17.09	15.38	1.1111833550065018
ExpectRevertTest.test_expectRevert_message()	20.23	18.1	1.1176795580110497
ExpectRevertTest.testFail_expectRevert_bytes4()	22.82	20.41	1.1180793728564429
ExpectRevertTest.testFail_expectRevert_multipleReverts()	19.66	17.05	1.1530791788856305
SymbolicStorageTest.testFail_SymbolicStorage1(uint256)	51.31	44.48	1.1535521582733814
SymbolicStorageTest.testFail_SymbolicStorage(uint256)	70.55	57.23	1.232745063777739
],uint256))	59.22	42.09	1.4069850320741268
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_merge_loop_heads	87.89	58.7	1.497274275979557
HevmTests.prove_revert	20.49	13.68	1.4978070175438596
FreshCheatcodes.test_address()	21.72	13.17	1.6492027334851935
TOTAL	847.32	775.91	1.0920338699075924

[geo2a]

KEVM performance at 4e78fe8

Test	4043-filter-smt-lemmas-for-predicate-checks time	master-79caf8c55 time	(4043-filter-smt-lemmas-for-predicate-checks/master-79caf8c55) time
mcd/dsvalue-read-pass-spec.k	60.21	62.7	0.9602870813397129
benchmarks/storagevar01-spec.k	49.31	47.19	1.0449247721974995
mcd-structured/pot-join-pass-rough-spec.k	201.05	182.56	1.1012817703768625
examples/erc20-spec.md	171.51	154.13	1.112761954194511
benchmarks/ecrecoverloop02-sig1-invalid-spec.k	118.25	99.96	1.1829731892757103
erc20/ds/transfer-success-1-spec.k	75.74	58.13	1.3029416824359192
examples/sum-to-n-spec.k	134.98	100.83	1.3386888822771
TOTAL	811.0500000000001	705.5	1.1496102055279944