#lang rosette
(require rosette/lib/synthax)


(define (polynomial x)
  (expt (+ 1 x) 5))


(define (poly-factor x)
  (+ (* (??) (expt x (??)))
     (* (??) (expt x (??)))
     (* (??) (expt x (??)))
     (* (??) (expt x (??)))
     (* (??) (expt x (??)))
     (* (??) (expt x (??)))))

(define (same p f x)
  (assert (= (p x) (f x))))

(define-symbolic i integer?)

(define binding
    (synthesize #:forall (list i) 
                #:guarantee (same polynomial poly-factor i)))


(print-forms binding)


sat-model: contract violation
  expected: sat?
  given: (unsat)