Inconsistent smtlib semantics?

[leepike]

> cd saw-script/doc/tutorial/code
> saw double.saw

Loading file "<PATH_TO>/saw-script/doc/tutorial/code/double.saw"
Valid
Valid
Valid
Done.

> cvc4 double.smt2
sat

But looking at double.saw, we are dumping to smtlib

let thm_neg = {{ \x -> ~(thm x) }};
write_smtlib2 "double.smt2" thm_neg;

where thm is what is proved by SAW. The tutorial text seems to suggest that thm_neg should be unsat when prove abc thm is Valid:

The new primitives introduced here are the tilde operator, ~, which constructs the logical negation of a term, and write_smtlib2, which writes a term as a proof obligation in SMT-Lib version 2 format. Because SMT solvers are satisfiability solvers, their default behavior is to treat free variables as existentially quantified. By negating the input term, we can instead treat the free variables as universally quantified: a result of “unsatisfiable” from the solver indicates that the original term (before negation) is a valid theorem. The prove primitive does this automatically, but for flexibility the write_smtlib2 primitive passes the given term through unchanged, because it might be used for either satisfiability or validity checking.

thm_neg generates the smtlib2 term

(forall ((s0 (_ BitVec 32)))
            (let ((s2 (bvmul s0 s1)))
            (let ((s4 (bvshl s0 s3)))
            (let ((s5 (= s2 s4)))
            (let ((s6 (not s5)))
            (not s6)))))))

(sat) and dumping thm generates

(forall ((s0 (_ BitVec 32)))
            (let ((s2 (bvmul s0 s1)))
            (let ((s4 (bvshl s0 s3)))
            (let ((s5 (= s2 s4)))
            (not s5))))))

(unsat).

[brianhuffman]

It seems we have made an odd number of negation errors. This will be easy to fix, but we should probably leave the ticket open until we have a regression test in place. We should also update the REPL documentation for write_smtlib2 to indicate which negation convention it's supposed to use. (I.e., do we interpret the argument like :prove or :sat in Cryptol?)

Alternatively, we could just remove the write_smtlib2 command completely, and recommend that people instead use sat or prove with offline_smtlib2 as a proof tactic. At least this way it is always obvious which convention the user wants.