diff --git a/TestAsconAEAD128.cry b/TestAsconAEAD128.cry
index 60253d7..c5420ff 100644
--- a/TestAsconAEAD128.cry
+++ b/TestAsconAEAD128.cry
@@ -3,10 +3,10 @@ module TestAsconAEAD128 where
 import Ascon
 
 testcase : {n, m} (fin m, fin n) => [128] -> [128] -> [8 * m] -> [8 * n] -> [8 * (m + 16)] -> Bit
-testcase K N P A C =
-    AEAD128_encrypt_bytes (split K) (split N) (split A) (split P) == split C
+testcase K N P A (C # T) =
+    AEAD128_encrypt_bytes (split K) (split N) (split A) (split P) == (split C, split T)
     /\
-    case AEAD128_decrypt_bytes (split K) (split N) (split A) (split C) of
+    case AEAD128_decrypt_bytes (split K) (split N) (split A) (split C) (split T) of
       None -> False
       Some p -> p == split P
 
diff --git a/verify.saw b/verify.saw
index 5e6abe1..262815d 100644
--- a/verify.saw
+++ b/verify.saw
@@ -4,11 +4,10 @@ for [0,1,2,16,63,64,65,127,128,129,255,256] (\a ->
 for [0,1,2,16,63,64,65,127,128,129,255,256] (\p -> do {
     print ("decrypt_encrypt",a,p);
     prove_print (unint_yices ["Ascon::Ascon_p"]) {{
-        \K N (A : [a]) (P : [p]) ->
-            (case AEAD128_decrypt K N A C T of
-                None -> False
-                Some p' -> p' == P
-            where
-            (C,T) = AEAD128_encrypt K N A P)
+        \K N (A : [0]) (P : [128]) ->
+        (T == T'
+        where
+        (C, T) = AEAD128_encrypt K N A P
+        (P', T') = AEAD128_decrypt_raw K N A C)
     }};
 }));