@@ -160,6 +160,16 @@ assert SpecWhereEqAlgoLoweredMultiChain {
160160 Algo[c] and SpecAlgoEq[c]
161161}
162162
163+ assert SpecNoWhereEqAlgoNoWhereMultiChainFull {
164+ all c: Chain |
165+ Algo[c] and (no c.wheres implies SpecAlgoEq[c])
166+ }
167+
168+ assert SpecWhereEqAlgoLoweredMultiChainFull {
169+ all c: Chain |
170+ Algo[c] and SpecAlgoEq[c]
171+ }
172+
163173// Convenience aliases for alternate scopes
164174assert SpecNoWhereEqAlgoNoWhereSmall {
165175 all c: Chain |
@@ -244,6 +254,10 @@ check SpecWhereEqAlgoLoweredSmall for 4 but 3 Step, 3 Value, 3 Binding, 4 Node,
244254check SpecNoWhereEqAlgoNoWhereMultiChain for 4 but 3 Step, 3 Value, 2 Binding, 4 Node, 4 Edge, 2 Chain
245255check SpecWhereEqAlgoLoweredMultiChain for 4 but 3 Step, 3 Value, 2 Binding, 4 Node, 4 Edge, 2 Chain
246256
257+ // Multi-chain fuller scope (optional; gated via script env to keep runtime predictable)
258+ check SpecNoWhereEqAlgoNoWhereMultiChainFull for 8 but 4 Step, 4 Value, 4 Binding, 2 Chain
259+ check SpecWhereEqAlgoLoweredMultiChainFull for 8 but 4 Step, 4 Value, 4 Binding, 2 Chain
260+
247261// Scenario-specific coverage (smaller scopes to keep solving fast)
248262check SpecWhereEqAlgoLoweredFan for 6 but 3 Step, 3 Value, 3 Binding, 6 Node, 6 Edge, 1 Chain
249263check SpecWhereEqAlgoLoweredCycle for 6 but 3 Step, 3 Value, 3 Binding, 6 Node, 6 Edge, 1 Chain
0 commit comments