internal error with private constants in rewrite rules

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 constants in rewrite rules #71

Closed steve-kremer closed 4 years ago

steve-kremer commented 4 years ago

The following file (bug.txt) triggers an internal error

Internal Error: Not_found

Note: the error is not triggered when removing the unused private constant s. However this is a minimal example obtained from a more complex example that does use s. I am also attaching the initial example (Passive-ActivityTracking-State.txt).

VincentCheval commented 4 years ago

It's related to the following enhancement #16 Private constants are not allowed in the right hand side of a rewrite rule but this condition is not tested yet.