Prove sorts, search & DP

[Grover-c13]

No description provided.

[github-actions]

bmc4j proof results

20 proofs → 18 matched expectation, 2 mismatched

Proof	Expected	Actual	Why it fails	Counterexample
SearchProof.interpolation_findsPresentKey_size4	VERIFIED	❌ REFUTED	java.lang.ArithmeticException: / by zero at InterpolationSearch.java:45 (InterpolationSearch.java:45) counterexample: key = 4L, start = 0, end = 3, pos = 0, a = [0, 1, 4, 4] replay: int start = 0; int end = 3; int pos = 0; int[] a = {0, 1, 4, 4}; // key: could not express integer value as a literal — inspect …	key = 4L, start = 0, end = 3, pos = 0, a = [0, 1, 4, 4]
SortSweepProof.gnomeSort_size4	VERIFIED	❌ UNKNOWN (PARSE_FAILURE)		this is NOT a refutati…
AliquotSumProof.getAliquotSum_defect_is_documented_not_engine_proven	VACUOUS	✅ VACUOUS	assumptions are unsatisfiable - this proof checks nothing no input satisfies every assume(...) — tighten or fix the assumptions (a contradictory pair, or a bound too small for the literals).	JBMC found com.thealgorithms.maths.AliquotSumProof.getAliquotSum_defect_is_documented_not_engine_proven VACUOUS ✗ assump…
BaselineProof.increment_grows_below_int_max	VERIFIED	✅ VERIFIED
CircleSortProof.circleSort_size3_returns_sorted_permutation	VERIFIED	✅ VERIFIED
DpSweepProof.coinChange_change_matches_bruteforce_twoCoins	VERIFIED	✅ VERIFIED
DpSweepProof.subsetSum_matches_bruteforce_n3	VERIFIED	✅ VERIFIED
MathSweepProof.binomial_symmetry_and_pascal	VERIFIED	✅ VERIFIED
MathSweepProof.digitalRoot_matches_mod9_closedForm	VERIFIED	✅ VERIFIED
MathSweepProof.gcd_divides_both_and_is_maximal	VERIFIED	✅ VERIFIED
MathSweepProof.genericRoot_matches_mod9_closedForm	VERIFIED	✅ VERIFIED
MathSweepProof.lcm_times_gcd_equals_product	VERIFIED	✅ VERIFIED
SearchProof.iterativeTernary_findsPresentKey_size4	VERIFIED	✅ VERIFIED
SearchProof.iterativeTernary_returnedIndexHoldsKey_size4	VERIFIED	✅ VERIFIED
SortSweepProof.circleSort_size4	VERIFIED	✅ VERIFIED
SortSweepProof.cocktailShakerSort_size4	VERIFIED	✅ VERIFIED
SortSweepProof.combSort_size4	VERIFIED	✅ VERIFIED
SortSweepProof.exchangeSort_size4	VERIFIED	✅ VERIFIED
SortSweepProof.oddEvenSort_size4	VERIFIED	✅ VERIFIED
SortSweepProof.pancakeSort_size4	VERIFIED	✅ VERIFIED