Booster implies: discharge leftover consequent obligations under the antecedent via SMT - #4156

Merged

ehildenb merged 9 commits into

implies-reasoning

Jun 18, 2026

Commits on Jun 16, 2026

kore-rpc-types, booster/Pattern/Implies, kore/JsonRpc: add indeterminate field on ImpliesResult

ehildenb
and
claude
committed
adbe4f8
booster/test/rpc-integration/{resources/implies-smt,test-implies-smt}, scripts/booster-integration-tests: add failing RPC tests for implies SMT discharge

ehildenb
and
claude
committed
6831148
booster/Pattern/Implies, test/rpc-integration/{test-implies-smt,test-implies2}: discharge consequent obligations under antecedent via SMT

ehildenb
and
claude
committed
c3178ba
booster/Pattern/Implies: consolidate ImpliesResult construction into a single mkResult builder

ehildenb
and
claude
committed
30a1f48

Commits on Jun 17, 2026