Synthesising with Grammar containing multiple instances of structs with different parameters returns unsat about rosette HOT 4 CLOSED

#lang rosette

(require rosette/lib/synthax rosette/lib/destruct)

(struct reg (id) #:transparent #:mutable)    
(struct BROADCAST (v0  size_o lane_size num_3 prec_i_o num_5 num_6 num_7) #:transparent)

(define broadcast-impl list)

(define (interpret prog env)
   (destruct prog
          [(reg id) (vector-ref-bv env id)]
            [ (BROADCAST v0 size_o lane_size num_3 prec_i_o num_5 num_6 num_7)                                                                                                                                                                                                                                                                                                                         
              (broadcast-impl (interpret v0 env) size_o lane_size                                                                                                                                                  
                                        num_3 prec_i_o num_5                                                                                                                                                                 
                                      num_6 num_7)                                                                                                                                                                         
             ]                  
   )
)

(define-grammar (base_2988_grammar_operations_tree)
                [expr 
                  (choose
                    (reg (bv 0 4)) 

                    (
                     BROADCAST
                     (expr) ;; 128-bit Bitvector operand
                     256				;; Integer Operand 
                     256				;; Lane Size 
                     256				;; Integer Operand 
                     16				;; Precision Operand 
                     0				;; Integer Operand 
                     0				;; Integer Operand 
                     0				;; Integer Operand 
                     )



                    (BROADCAST (expr) ; <1 x i32>
                     512  512  512  32  0  0  0  )


                    )]
                )

(define bounded-grammar
  (base_2988_grammar_operations_tree  #:depth 2 )
  )

(define-symbolic sym-bv (bitvector 32))
(define env (vector sym-bv))

(define broadcast-expr 
  (BROADCAST (reg (bv 0 4)) ; <1 x i32>
                          512  512  512  32  0  0  0  )
  )


;; Result takes sym-bv  and concatenates
;; to itself 16 times
(define result (interpret broadcast-expr env))

(define sol?
  (synthesize
    #:forall (list  env)
    #:guarantee 
    (begin 
      (assert
        (equal?   result (interpret bounded-grammar env))
        )
      )
    ) 
  )

(displayln "Synthesizing Complete!")
(define satisfiable? (sat? sol?))


(define materialize 
  (if satisfiable? 
    (evaluate bounded-grammar sol?)
    '()
    )
  )

(displayln "Synthesized solution")
(println materialize)

 (define (broadcast-impl  a %vectsize %lanesize1 %lanesize2 %elemsize %laneoffset %arg0 %arg1 )
   (define dst
      (apply
        concat
       (for/list ([%outer.it (reverse (range 0 %vectsize %lanesize1))]) ; 0 256 256 => 1
                 (apply
                    concat
                    (for/list ([j0.new (reverse (range %laneoffset %lanesize2 %elemsize))]) ; 0 256 16 => 16
                             (define %lastidx1 (-  %elemsize  1)) ; 15
                           (define %highidx0 (+  %lastidx1  %arg0)) ; 15 + 0 = 15
                            (define %1 (extract  %highidx0 %arg0 a)) ; 15 0 => first 16 bits
                            %1
                            )
                  )
                )
      )
     )
  dot
   )