addsimp could do more input checking; printing should not exit the REPL

[msaaltink]

OK, I understand that this is an error on my part, adding a theorem that is not an equality to a simpset. That said, it is unfriendly of SAW to exit the REPL after printing this error message.

sawscript> t <- prove_print z3 {{ 1 > 0x0 }};
Valid
sawscript> ss1 <- addsimp t (cryptol_ss ())
sawscript> ss1
Rewrite Rules
=============
saw: ruleOfProp: Predicate not an equation: let { x@1 = Cryptol.TCNum 4
x@2 = Prelude.Vec 4 Prelude.Bool
x@3 = Cryptol.PLiteralSeqBool x@1
}
in Cryptol.ecGt x@2 (Cryptol.PCmpSeqBool x@1)
(Cryptol.ecNumber (Cryptol.TCNum 1) x@2 x@3)
(Cryptol.ecNumber (Cryptol.TCNum 0) x@2 x@3)
CallStack (from HasCallStack):
error, called at src/Verifier/SAW/Rewriter.hs:306:16 in saw-core-0.1-25ujyDMdmUBFqb9n24Ud3k:Verifier.SAW.Rewriter
$

[brianhuffman]

As of #954, this error no longer causes the REPL to exit. What we should do is make the error checking happen in addsimp instead of during printing.