uw-unsat / serval-tutorial-sosp19

13 stars 3 forks source link

serval/lib/debug.rkt:8:14: asserts: unbound identifier #3

Closed Archfx closed 1 year ago

Archfx commented 1 year ago

make verify-monitor command yields an unbounded identifier in the debug.rkt line 8. This corresponds to the (&& (null? (asserts)) statement.

Is there anything that I am missing?

#lang rosette

(provide (all-defined-out))

(define target-spectre (make-parameter #f))

(define (concrete?)
  (&& (null? (asserts))
      (equal? #t (pc))))

(define assert-db (make-hash))
 ....

Thanks in advance!!

Archfx commented 1 year ago

Cloned serval from the serval repo fixed the issue.