#lang rosette/safe (define-symbolic anint integer?) (define anint2 10) (define (plusone x) (+ x 1)) ;(current-bitwidth #f) (define mypredicate (<= (plusone anint) 0)) ;(solve (assert mypredicate)) ;(verify (assert mypredicate)) ;(verify (assert (forall (list anint) mypredicate))) (require rosette/lib/synthax) (define (f x) ((choose + - *) x (??))) (define goal (implies (>= anint 0) (> (f anint) 2))) (current-bitwidth #f) ;(generate-forms (synthesize #:forall (list anint) #:guarantee (assert goal));) (f anint)