rw1nd Goto Github PK

#lang rosette
(define-symbolic* hello integer? #:length 5)
(define sol
   (solve
     (assert (&&
               (= (list-ref hello 0) 104)
               (= (list-ref hello 1) 101)
               (= (list-ref hello 2) 108)
               (= (list-ref hello 3) 108)
               (= (list-ref hello 4) 111)))))
(print
  (list->string
   (map integer->char (evaluate hello sol))))