Project

General

Profile

« Previous | Next » 

Revision dccec723

Added by Lélio Brun over 3 years ago

a version that almost work for the k-inuctive two_counters example

View differences:

src/causality.ml
475 475 
              match nd.node_spec with
476 476 
              | None ->
477 477 
                []
478 
              | Some (NodeSpec (id, _)) ->
478 
              | Some (NodeSpec id) ->
479 479 
                [ id ]
480 480 
              | Some (Contract c) ->
481 481 
                get_contract_calls (fun _ -> true) c

Also available in: Unified diff