offline_smtlib2 generates wrong output

[brianhuffman]

When we use prove (offline_smtlib2 "filename"), it should result in a file containing the same query it would have sent to a solver had you typed prove z3. But that's not what you get.
Here's an example with a predicate that does not hold for all x:

sawscript> prove (offline_smtlib2 "foo") {{ \(x:[8]) -> x == 13 }}
[21:53:39.990] Valid
sawscript> :q

~/Work/saw-script$ z3 foo.prove0.smt2
success
success
success
success
success
success
unsat

~/Work/saw-script$ cat foo.prove0.smt2
; Automatically created by SBV on 2019-12-12 13:53:39.982407 PST
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic BV)
; --- uninterpreted sorts ---
; --- tuples ---
; --- sums ---
; --- literal constants ---
(define-fun s1 () (_ BitVec 8) #x0d)
; --- skolem constants ---
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(assert (forall ((s0 (_ BitVec 8)))
            (let ((s2 (= s0 s1)))
            (not s2))))
(check-sat)

I was trying to prove forall x, x == 13, and it generated an smt file that returns unsat if it can prove exists x, x == 13. This is wrong.

[brianhuffman]

It looks like I tried to fix this before in 5198051, and while that fix solved a logical negation problem, it accidentally switched the quantifiers at the same time.