Decomposed feasibility proof obligations into independant clauses. The former formulation for an assignment to two variables was: (∃ x',y':: x' = E ∧ y' = F) but now this will be two separate proof obligations: (∃ x':: x' = E) and (∃ y':: y' = F) unless an assignment refers to more than one primed variable.

It proceeds by partitioning primed variables and expressions into as many partition as possible so that expressions are in the same partition as all the primed variables it refers to. Each partition then form an existential quantification.

Finally, any assignment of the form P ∧ Q is broken down into two assignments.
Changed the automatic compilation program to allow the user to browse through the error messages using the unix command 'less'.
Added a test for the partitioning algorithm and found and fixed a major error
changed the trigger of the periodic tester to make a test triggered under two necessary conditions: a source or test file must have changed and the test binary must be more recent than the test results.
split the initialization feasibility proof obligation into independent components.
improved the trigger of the continuous tester so that compiling "test" during while the tests are running triggers a round of tests.