internal error with private function in determinate processes

DeepSec-prover / deepsec

DEciding Equivalence Properties in SECurity protocols

GNU General Public License v3.0

17 stars 2 forks source link

internal error with private function in determinate processes #75

Open irakoton opened 4 years ago

irakoton commented 4 years ago

The following file (bug.txt) triggers Internal Error: [process_determinate.ml >> find_one_action] Should not be applied on a nil process. When trying different variations, the internal error does not appear when the process is not determinate or if the function g is not private.

Tested on branches master and fix_bug_67_to_72.