@@ -894,12 +894,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
894
894
pragma [ nomagic]
895
895
predicate revFlow ( NodeEx node ) { revFlow ( node , _) }
896
896
897
- pragma [ nomagic]
898
- predicate revFlowAp ( NodeEx node , Ap ap ) {
899
- revFlow ( node ) and
900
- exists ( ap )
901
- }
902
-
903
897
bindingset [ node, state]
904
898
predicate revFlow ( NodeEx node , FlowState state , Ap ap ) {
905
899
revFlow ( node , _) and
@@ -1278,8 +1272,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1278
1272
1279
1273
predicate revFlow ( NodeEx node ) ;
1280
1274
1281
- predicate revFlowAp ( NodeEx node , Ap ap ) ;
1282
-
1283
1275
bindingset [ node, state]
1284
1276
predicate revFlow ( NodeEx node , FlowState state , Ap ap ) ;
1285
1277
@@ -2456,16 +2448,11 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2456
2448
)
2457
2449
}
2458
2450
2459
- additional predicate revFlow ( NodeEx node , FlowState state ) { revFlow ( node , state , _, _, _) }
2460
-
2461
2451
predicate revFlow ( NodeEx node , FlowState state , Ap ap ) { revFlow ( node , state , _, _, ap ) }
2462
2452
2463
2453
pragma [ nomagic]
2464
2454
predicate revFlow ( NodeEx node ) { revFlow ( node , _, _, _, _) }
2465
2455
2466
- pragma [ nomagic]
2467
- predicate revFlowAp ( NodeEx node , Ap ap ) { revFlow ( node , _, _, _, ap ) }
2468
-
2469
2456
private predicate fwdConsCand ( Content c , Ap ap ) { storeStepFwd ( _, ap , c , _, _) }
2470
2457
2471
2458
private predicate revConsCand ( Content c , Ap ap ) {
@@ -2620,7 +2607,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2620
2607
*/
2621
2608
private class FlowCheckNode extends NodeEx {
2622
2609
FlowCheckNode ( ) {
2623
- revFlow ( this , _ , _ ) and
2610
+ revFlow ( this ) and
2624
2611
(
2625
2612
flowCheckNode ( this ) or
2626
2613
Config:: neverSkip ( this .asNode ( ) )
0 commit comments