Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real division
SMT-LIB printer updates (some missing cases).
Merge branch '1.2.x'
some work on abs
finish absolute value