From a0bb572388e5eda059f9909cb1e84b328b11974c Mon Sep 17 00:00:00 2001
From: "Adam C. Foltzer" <acfoltzer@galois.com>
Date: Mon, 8 Sep 2014 14:45:01 -0700
Subject: [PATCH] add note about solvers for ZUC theorem

---
 examples/ZUC.cry | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/examples/ZUC.cry b/examples/ZUC.cry
index ec7ab09c..f32d8295 100644
--- a/examples/ZUC.cry
+++ b/examples/ZUC.cry
@@ -300,7 +300,9 @@ property LoadKey_TestVectors =
 // cuts down on the problem size and is sufficient to ensure the iv's will be
 // the same. That is, if this theorem fails, then so would the final iv's used
 // by ZUC.
-property ZUC_isResistantToCollisionAttack (k, iv1, iv2) =
+//
+// Use a solver other than CVC4; Z3 and Boolector do it quickly.
+property ZUC_isResistantToCollisionAttack k iv1 iv2 =
     if iv1 != iv2
     then InitializeZUC (k, iv1) @ 1 != InitializeZUC (k, iv2) @ 1
     else True