Closed bpowers closed 7 years ago
Without this, the library throws an exception when Z3 graces us with a model like:
(model (define-fun stack_base () Int (- 128)) (define-fun stack_max () Int 0) )
Without this, the library throws an exception when Z3 graces us with a model like: