ok, forked Z3 bits into smtZ3
now populate the SMTSOLVER sig in proverArch.ml