DeepSec-prover / deepsec

DEciding Equivalence Properties in SECurity protocols
GNU General Public License v3.0
17 stars 2 forks source link

Problem with if-then-else in determinate when the then branch is not accessible #77

Open VincentCheval opened 4 years ago

VincentCheval commented 4 years ago

In determinate process, there is an optimisation that does not generate constraint systems for else-branch when all the else branches are 0. However it is problematic when the then branch is not accessible as it would generate an error if matched with a process that does not have an if-then-else test.

ifthenelse_determinate.txt