<div dir="ltr">I tried writing a small program, but got stuck pretty early on. When I try verifying the "divides?" function below, the tool times out. What's happening?<div><br></div><div>(module div racket<br></div><div><div>  (provide (contract-out [divides? (-> positive? positive? boolean?)]))</div><div><br></div><div>  (define (positive? x)</div><div>    (and (integer? x) (<= 0 x)))</div><div>  </div><div>  (define (divides? a b)</div><div>    (cond [(= 0 b) #t]</div><div>          [(< b a) #f]</div><div>          [else (divides? a (- b a))]))</div><div><br></div><div>)</div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jan 15, 2015 at 3:14 PM, David Van Horn <span dir="ltr"><<a href="mailto:dvanhorn@cs.umd.edu" target="_blank">dvanhorn@cs.umd.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 1/15/15, 2:48 PM, Robby Findler wrote:<br>
> Can you randomly make up programs from your grammar, get example<br>
> errors from the tool, and then run those programs to see if you<br>
> find bugs in the analysis like that one?<br>
<br>
</span>Yes, we're planning to do this.<br>
<span class=""><br>
> That said, I don't see how the bug in >=/c is coming in here. Can<br>
> you explain more?<br>
<br>
</span>On further inspection, the counterexample is wrong.  (There are<br>
counterexamples due to the model of >=/c, but the one that reported is<br>
not an actual one.)  This will be fixed shortly.<br>
<div class="HOEnZb"><div class="h5"><br>
David<br>
<br>
_________________________<br>
  Racket Developers list:<br>
  <a href="http://lists.racket-lang.org/dev" target="_blank">http://lists.racket-lang.org/dev</a><br>
</div></div></blockquote></div><br></div>