remove some dead code
reverted the behaviour of Smt.say to rewrite * into /\

instead of telling Z3 that forall x y, x * y = x /\ y

With the former, trivial tests such as tests/check_tests/test0[23].star
took 10 to 50 seconds to run! Now they take < 1s.

Unless that turns out to be a bug in my version of Z3 (didn't try
others)...