Regression timing and version number update

tamarin-prover · Aug 30, 2023 · f172d7f · f172d7f
1 parent 93c7165
commit f172d7f
Show file tree

Hide file tree

Showing 313 changed files with 1,219 additions and 1,204 deletions.
diff --git a/case-studies-regression/Tutorial_analyzed.spthy b/case-studies-regression/Tutorial_analyzed.spthy
@@ -242,10 +242,10 @@ qed
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end

diff --git a/case-studies-regression/ake/bilinear/Chen_Kudla_analyzed.spthy b/case-studies-regression/ake/bilinear/Chen_Kudla_analyzed.spthy
@@ -2610,10 +2610,10 @@ Failed to derive Variable(s): ~msk
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -2628,7 +2628,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/Chen_Kudla.spthy
 
   output:          examples/ake/bilinear/Chen_Kudla.spthy.tmp
-  processing time: 35.44s
+  processing time: 28.17s
 
   WARNING: 1 wellformedness check failed!
            The analysis results might be wrong!

diff --git a/case-studies-regression/ake/bilinear/Chen_Kudla_eCK_analyzed.spthy b/case-studies-regression/ake/bilinear/Chen_Kudla_eCK_analyzed.spthy
@@ -539,10 +539,10 @@ Failed to derive Variable(s): ~msk
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -557,7 +557,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/Chen_Kudla_eCK.spthy
 
   output:          examples/ake/bilinear/Chen_Kudla_eCK.spthy.tmp
-  processing time: 22.66s
+  processing time: 23.41s
 
   WARNING: 1 wellformedness check failed!
            The analysis results might be wrong!

diff --git a/case-studies-regression/ake/bilinear/Joux_EphkRev_analyzed.spthy b/case-studies-regression/ake/bilinear/Joux_EphkRev_analyzed.spthy
@@ -1061,10 +1061,10 @@ Failed to derive Variable(s): ltkB, ltkC
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -1079,7 +1079,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/Joux_EphkRev.spthy
 
   output:          examples/ake/bilinear/Joux_EphkRev.spthy.tmp
-  processing time: 13.03s
+  processing time: 11.39s
 
   WARNING: 1 wellformedness check failed!
            The analysis results might be wrong!

diff --git a/case-studies-regression/ake/bilinear/Joux_analyzed.spthy b/case-studies-regression/ake/bilinear/Joux_analyzed.spthy
@@ -1077,10 +1077,10 @@ Failed to derive Variable(s): ltkB, ltkC
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -1095,7 +1095,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/Joux.spthy
 
   output:          examples/ake/bilinear/Joux.spthy.tmp
-  processing time: 9.57s
+  processing time: 9.86s
 
   WARNING: 1 wellformedness check failed!
            The analysis results might be wrong!

diff --git a/case-studies-regression/ake/bilinear/RYY_PFS_analyzed.spthy b/case-studies-regression/ake/bilinear/RYY_PFS_analyzed.spthy
@@ -424,10 +424,10 @@ qed
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -442,7 +442,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/RYY_PFS.spthy
 
   output:          examples/ake/bilinear/RYY_PFS.spthy.tmp
-  processing time: 3.59s
+  processing time: 3.97s
 
   key_agreement_reachable (exists-trace): verified (11 steps)
   key_secrecy_PFS (all-traces): falsified - found trace (12 steps)

diff --git a/case-studies-regression/ake/bilinear/RYY_analyzed.spthy b/case-studies-regression/ake/bilinear/RYY_analyzed.spthy
@@ -554,10 +554,10 @@ qed
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -572,7 +572,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/RYY.spthy
 
   output:          examples/ake/bilinear/RYY.spthy.tmp
-  processing time: 4.20s
+  processing time: 3.81s
 
   key_agreement_reachable (exists-trace): verified (11 steps)
   key_secrecy_WPFS (all-traces): verified (53 steps)

diff --git a/case-studies-regression/ake/bilinear/Scott_EphkRev_analyzed.spthy b/case-studies-regression/ake/bilinear/Scott_EphkRev_analyzed.spthy
@@ -304,10 +304,10 @@ Failed to derive Variable(s): ~s
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -322,7 +322,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/Scott_EphkRev.spthy
 
   output:          examples/ake/bilinear/Scott_EphkRev.spthy.tmp
-  processing time: 6.85s
+  processing time: 7.96s
 
   WARNING: 1 wellformedness check failed!
            The analysis results might be wrong!

diff --git a/case-studies-regression/ake/bilinear/Scott_analyzed.spthy b/case-studies-regression/ake/bilinear/Scott_analyzed.spthy
@@ -1842,10 +1842,10 @@ Failed to derive Variable(s): ~s
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -1860,7 +1860,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/Scott.spthy
 
   output:          examples/ake/bilinear/Scott.spthy.tmp
-  processing time: 9.62s
+  processing time: 10.37s
 
   WARNING: 1 wellformedness check failed!
            The analysis results might be wrong!

diff --git a/case-studies-regression/ake/bilinear/TAK1_analyzed.spthy b/case-studies-regression/ake/bilinear/TAK1_analyzed.spthy
@@ -2674,10 +2674,10 @@ Failed to derive Variable(s): ~eb, ~ec, XB, XC
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -2692,7 +2692,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/TAK1.spthy
 
   output:          examples/ake/bilinear/TAK1.spthy.tmp
-  processing time: 28.80s
+  processing time: 30.04s
 
   WARNING: 1 wellformedness check failed!
            The analysis results might be wrong!

diff --git a/case-studies-regression/ake/bilinear/TAK1_eCK_like_analyzed.spthy b/case-studies-regression/ake/bilinear/TAK1_eCK_like_analyzed.spthy
@@ -552,10 +552,10 @@ Failed to derive Variable(s): ~eb, ~ec, XB, XC
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -570,7 +570,7 @@ summary of summaries:
 analyzed: examples/ake/bilinear/TAK1_eCK_like.spthy
 
   output:          examples/ake/bilinear/TAK1_eCK_like.spthy.tmp
-  processing time: 36.61s
+  processing time: 38.21s
 
   WARNING: 1 wellformedness check failed!
            The analysis results might be wrong!

diff --git a/...-studies-regression/ake/dh/DHKEA_NAXOS_C_eCK_PFS_keyreg_partially_matching_analyzed.spthy b/...-studies-regression/ake/dh/DHKEA_NAXOS_C_eCK_PFS_keyreg_partially_matching_analyzed.spthy
@@ -5268,10 +5268,10 @@ Derivation Checks
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -5286,7 +5286,7 @@ summary of summaries:
 analyzed: examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_keyreg_partially_matching.spthy
 
   output:          examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_keyreg_partially_matching.spthy.tmp
-  processing time: 63.11s
+  processing time: 63.85s
 
   WARNING: 1 wellformedness check failed!
            The analysis results might be wrong!

diff --git a/case-studies-regression/ake/dh/DHKEA_NAXOS_C_eCK_PFS_partially_matching_analyzed.spthy b/case-studies-regression/ake/dh/DHKEA_NAXOS_C_eCK_PFS_partially_matching_analyzed.spthy
@@ -5223,10 +5223,10 @@ Derivation Checks
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -5241,7 +5241,7 @@ summary of summaries:
 analyzed: examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_partially_matching.spthy
 
   output:          examples/ake/dh/DHKEA_NAXOS_C_eCK_PFS_partially_matching.spthy.tmp
-  processing time: 59.23s
+  processing time: 46.60s
 
   WARNING: 1 wellformedness check failed!
            The analysis results might be wrong!

diff --git a/case-studies-regression/ake/dh/NAXOS_eCK_PFS_analyzed.spthy b/case-studies-regression/ake/dh/NAXOS_eCK_PFS_analyzed.spthy
@@ -385,10 +385,10 @@ Failed to derive Variable(s): ~lkI
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -403,7 +403,7 @@ summary of summaries:
 analyzed: examples/ake/dh/NAXOS_eCK_PFS.spthy
 
   output:          examples/ake/dh/NAXOS_eCK_PFS.spthy.tmp
-  processing time: 1.53s
+  processing time: 1.49s
 
   WARNING: 1 wellformedness check failed!
            The analysis results might be wrong!

diff --git a/case-studies-regression/ake/dh/NAXOS_eCK_analyzed.spthy b/case-studies-regression/ake/dh/NAXOS_eCK_analyzed.spthy
@@ -759,10 +759,10 @@ Failed to derive Variable(s): ~lkI
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -777,7 +777,7 @@ summary of summaries:
 analyzed: examples/ake/dh/NAXOS_eCK.spthy
 
   output:          examples/ake/dh/NAXOS_eCK.spthy.tmp
-  processing time: 2.09s
+  processing time: 1.79s
 
   WARNING: 1 wellformedness check failed!
            The analysis results might be wrong!

diff --git a/case-studies-regression/ake/dh/UM_one_pass_attack_analyzed.spthy b/case-studies-regression/ake/dh/UM_one_pass_attack_analyzed.spthy
@@ -353,10 +353,10 @@ Failed to derive Variable(s): ~ea
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -371,7 +371,7 @@ summary of summaries:
 analyzed: examples/ake/dh/UM_one_pass_attack.spthy
 
   output:          examples/ake/dh/UM_one_pass_attack.spthy.tmp
-  processing time: 2.39s
+  processing time: 1.59s
 
   WARNING: 1 wellformedness check failed!
            The analysis results might be wrong!

diff --git a/case-studies-regression/ake/dh/UM_one_pass_fix_analyzed.spthy b/case-studies-regression/ake/dh/UM_one_pass_fix_analyzed.spthy
@@ -821,10 +821,10 @@ Failed to derive Variable(s): ~ea
 
 /*
 Generated from:
-Tamarin version 1.7.1
+Tamarin version 1.8.0
 Maude version 3.2.1
-Git revision: af08d7fd0eaf723c6981fa57abca5c0b7e24a560, branch: subterm-new
-Compiled at: 2023-07-31 09:45:04.338688526 UTC
+Git revision: 93c7165df1b26f607b8475e26d3a7e0d54f295cb, branch: master
+Compiled at: 2023-08-29 12:56:59.317473841 UTC
 */
 
 end
@@ -839,7 +839,7 @@ summary of summaries:
 analyzed: examples/ake/dh/UM_one_pass_fix.spthy
 
   output:          examples/ake/dh/UM_one_pass_fix.spthy.tmp
-  processing time: 1.15s
+  processing time: 1.05s
 
   WARNING: 1 wellformedness check failed!
            The analysis results might be wrong!