somewhat working
minor fix
some printing to smtlib functions