Just curious: the value of src is the top-level symbolic variable A, B, or C. Should that be (state-A s), state-B, or state-C instead?

(I don't know what you want to do, so it could be that what you have is really what you want already... but in case you are modeling register assignment based on the previous state, what you currently have doesn't make sense to me)

Quite right! Thanks for noticing that. Updated accordingly (same result)

I have a working code on my laptop, but the battery ran out... I'll post it when I get back home.

It's long ago that I read define-grammar, but if I remember correctly, the "top level" of each clause should be stuff like (choose ...) or (??).

In any case, here's a repaired code that synthesizes swap

#lang rosette/safe

(require rosette/lib/synthax)

(define-symbolic A B C integer?)
(struct state (A B C) #:transparent)

; sketch
(define (mover s)
  (synthesized s #:depth 3))

; checker
; implements B = A
(define (check-mover impl s)
  (define result (impl s))
  (assert (= (state-B result) (state-A s)))
  (assert (= (state-A result) (state-B s))))

; an example that passes check-mover
(define (moveBtoA s)
  (state (state-A s) (state-A s) (state-C s)))

#;
(check-mover moveBtoA (state 11 12 13))

(define (do-move s srcno dstno)
  ; restrict values
  (assert (and (>= dstno 0) (< dstno 3)
               (>= srcno 0) (< srcno 3)))
  (define src
    (case srcno
      [(0) (state-A s)]
      [(1) (state-B s)]
      [(2) (state-C s)]))
  ; perform a move from A, B, or C to A, B, or C determined by two integers
  (state (if (= dstno 0) src (state-A s))
         (if (= dstno 1) src (state-B s))
         (if (= dstno 2) src (state-C s))))

(define-grammar (synthesized s)
  [expr
   (choose
    s
    (do-move (expr) (??) (??)))])

(define sol
  (synthesize
   #:forall (list A B C)
   #:guarantee (check-mover mover (state A B C))))

(if (sat? sol) (print-forms sol) (print "UNSAT"))

Thank you so much for your quick response and for providing a solution. I'm still not certain what rule I should apply in the future to avoid this mistake, though. Can you explain in more detail what was wrong with my original code? I have other working examples where the (??) and (choose... structures appear at various levels in the grammar without a problem, and I can't tell what rule the code in this issue violates.

Also, is there a reason for the result? It's very odd that Rosette should provide a "sat" result and then supply a form that has the name of a grammar rule in it. How can that work?

I found a small change to my original code that makes it work:

    ; PROBLEM AREA
   (let ((srcno (??))
         (dstno (??)))
     ; restrict values
     (assert (and (>= dstno 0) (< dstno 3)
                  (>= srcno 0) (< srcno 3)))
     (lambda (s)
     ; perform a move from A, B, or C to A, B, or C determined by two integers
       (let ((src (if (= srcno 0) (state-A s)
                      (if (= srcno 1) (state-B s) (state-C s)))))
         (state (if (= dstno 0) src (state-A s))
                (if (= dstno 1) src (state-B s))
                (if (= dstno 2) src (state-C s)))))

Here the (??) structures are pulled outside of the lambda. I understand that these forms may produce a different symbolic value each time they are evaluated. Could that cause a problem?