#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))))
rw1nd Goto Github PK
Name: Jian Fang
Type: User
Bio: I' m interesting in software verification.
Location: Beijing, China
Blog: rw1nd.github.io