sunshowers / z3.rkt

Racket bindings for Z3
BSD 2-Clause "Simplified" License
19 stars 11 forks source link

Get error with `regexp-replace*` when running test #1

Open philnguyen opened 8 years ago

philnguyen commented 8 years ago

When I try running a test case directly, e.g. one in test-integers.rkt:

(smt:with-context
    (smt:new-context)
    (smt:declare-fun a () Int)
    (smt:assert (>/s a 10))
    (smt:assert (</s a 20))
    (check-eq? (smt:check-sat) 'sat)
    (define a-eval (smt:eval a))
    (check-true (and (> a-eval 10) (< a-eval 20)))
    (smt:assert (=/s (+/s a 5) 14))
    (check-eq? (smt:check-sat) 'unsat))

I get this error:

; regexp-replace*: contract violation
;   expected: (or/c string? bytes?)
;   given: 'mk-config
;   argument position: 2nd
;   other arguments...:
;    #rx"-"
;    "_"

This is Racket 6.5 and Z3 4.4.1

wenkokke commented 3 years ago

@philnguyen Did you ever fix this error, while porting the library to Typed Racket?

philnguyen commented 3 years ago

Not that I remember :)