diff --git a/lib/CryptolTC.z3 b/lib/CryptolTC.z3 index f48923f1d..391a85151 100644 --- a/lib/CryptolTC.z3 +++ b/lib/CryptolTC.z3 @@ -327,14 +327,14 @@ ; (declare-fun L () InfNat) ; (declare-fun w () InfNat) -; +; ; (assert (cryVar L)) ; (assert (cryVar w)) -; +; ; (assert (cryAssume (cryFin w))) ; (assert (cryAssume (cryGeq w (cryNat 1)))) ; (assert (cryAssume (cryGeq (cryMul (cryNat 2) w) (cryWidth L)))) -; +; ; (assert (cryProve ; (cryGeq ; (cryMul @@ -343,7 +343,7 @@ ; (cryMul (cryNat 16) w)) ; (cryMul (cryNat 16) w)) ; (cryAdd (cryNat 1) (cryAdd L (cryMul (cryNat 2) w)))))) -; +; ; (check-sat)