This is a program for executing algorithm specifications written in firstorder predicate language with variables ranging over the integers and functions from the integers to the integers (which can model arrays). The solver then searches for a satisfying assignment of a given input formula. Downloads
