Failure in test_tutorial5

[atomb]

Running the tests in intTests/test_tutorial5 currently fails with a log ending in

[16:37:33.347] Loading file "/Users/atomb/galois/saw-script/intTests/test_tutorial5/tmp/des3.saw"
[warning] at ./DES.cry:25:9--25:13
    This binding for last shadows the existing binding from
    (at /var/folders/n8/s7z9ns8d4k39v2y_2sn__12m0000gp/T/Cryptol91292-0.cry:561:1--561:5, last)
[warning] at ./DES.cry:25:16--25:38:
  Defaulting type argument 'ix' of '(Cryptol::@)' to max 1
                                                         (width ?n`1054)
  where
  ?n`1054 is length of comprehension generator at ./DES.cry:22:15--24:35
[16:37:33.444] proving dec_enc...
[16:37:37.201] Valid
[16:37:37.201] proving enc_dec...
[16:37:41.307] Valid
[16:37:41.307] Theorem (let { x@1 = Prelude.Vec 64 Prelude.Bool
    }
 in (key : x@1)
-> (msg : x@1)
-> Prelude.EqTrue (prop2 key msg))
[16:37:41.337] proving dec3_enc3...
[16:37:41.369] ruleOfProp: Predicate not an equation: prop1 !1 !0
CallStack (from HasCallStack):
  error, called at src/Verifier/SAW/Rewriter.hs:306:16 in saw-core-0.1-LR0ijpUgX5Z4WRirnlruYt:Verifier.SAW.Rewriter

[brianhuffman]

As far as I can tell, the problematic sawscript file doc/tutorial/code/des3.saw has never worked. (It has never been modified since it was added in commit 2890780.) Also, it clearly shouldn't work, as it tries to use a theorem of the form forall x y, prop1 x y (which is not an equation) as a rewrite rule. des3.saw should be rewritten to make it work properly.