Hello everybody, not sure if this is the good place to ask about this but I couldn't find a good location so I'm asking for help here, after all it's strongly connected to Racket :)
I'm trying to reverse-engineer some specific piece of hardware with the help of Rosette, to discover if it can help or not. In the long run I want it to help me find magic numbers for a specific routine to match captures of the hardware output (can't say more about this though). After dumbing down (a lot) my first tries, I'm having issues with this code running endlessly: #lang rosette/safe (define (zero-a x) 0) (define (zero-b x) (if (= x 0) 0 (zero-b (- x 1)))) (define-symbolic x integer?) (assert (>= x 0)) (assert (<= x 10)) (verify (assert (= (zero-a x) (zero-b x)))) I don't have a strong theoretical understanding of what Rosette can and cannot do, but I thought that by restraining the range with the asserts, at least I'd get a brute force search of the solution space, which should be fast. Does it make sense ? Can somebody explain me where is my misunderstanding ? Thank you folks, Bertrand -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAHV%3D05otPXjbrEaHWvJF-SeDSxz2-Mjq3p%3DSHR3HvuJRAJJ3-A%40mail.gmail.com.
