MAYBE
UNSAT
user error ("/tmp/SMTS16139470411043995593" (line 142, column 15):
unexpected "_"
expecting digit or ")")