defining a prop before verify results in different behavior than just verify

[dbp]

This may be expected behavior, but it surprised me based on the docs -- is there an explanation of why this is the case? Sorry for not having a smaller reproduction. The commented out code (incorrectly) says its unsatisfiable, whereas the uncommented verification (correctly) finds a counterexample.

(define (badsort l)
  (cond [(empty? l) l]
        [(cons? l)
         (badsert (first l)
                  (badsort (rest l)))]))

(define (badsert x l)
  (cond [(empty? l) (list x)]
        [(cons? l)
         (if (< x (first l))
             (cons x l)
             (badsert x (rest l)))]))

(define-symbolic a b c d e n integer?)
(define xs (take (list a b c d e) n))

;(define bad-prop (assert (eq? (length xs) (length (badsort xs)))))
;(verify bad-prop) ; unsat

(verify (assert (eq? (length xs) (length (badsort xs)))))

[sorawee]

According to the doc:

Formally, (verify expr) searches for a model of the formula (vc-assumes P) ∧ (vc-asserts P) ∧ (vc-assumes Q) ∧ ¬ (vc-asserts Q), where P is the verification condition before the call to verify and Q is the verification condition generated by evaluating expr.

(define bad-prop (assert (eq? (length xs) (length (badsort xs))))) changes the vc before the call to verify (P), and you don't want to do that.

In contrast, (verify (assert (eq? (length xs) (length (badsort xs))))) changes the vc during the evaluation of (verify ...) (Q), which is what you want to do.

[dbp]

Ah, I see. Thanks for the (very quick) clarification. The statefulness of this has been somewhat confusing to me, but I think I'm starting to figure it out :)