z3 is something I didn't know about until encountering it here. Spent the last few hours playing with the solver, it's quite interesting especially since I've

z3 is something I didn't know about until encountering it here. Spent the last few hours playing with the solver, it's quite interesting especially since I've had a fair amount of exposure to Scheme. Felt right at home after getting it up and running. Glitch-free compiling and installing under FreeBSD. The only problem was finding documentation. Rise4fun.com is mentioned in another post, the exact URL for getting started is http://rise4fun.com/Z3/tutorial/guide http://rise4fun.com/Z3/tutorial/guide. Also, very useful information here-- http://www.smt-lib.org/ http://www.smt-lib.org/