HolSmt: parse div0 and mod0 in Z3 proofs

Unfortunately, these operators don't seem to be documented.

However, from a quick reading of the Z3 source code, it seems that
they seem to be similar to `div` and `mod`, but they seem to be used
to indicate that Z3 can't prove that the divisor is non-zero.

src/HolSmt/SmtLib_Theories.sml

@@ -337,8 +337,12 @@ in
       ("*", leftassoc intSyntax.mk_mult),
       ("div", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
         (Term.prim_mk_const {Thy="HolSmt", Name="smtdiv"}, t1), t2))),
+      ("div0", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
+        (Term.prim_mk_const {Thy="HolSmt", Name="smtdiv"}, t1), t2))),
       ("mod", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
         (Term.prim_mk_const {Thy="HolSmt", Name="smtmod"}, t1), t2))),
+      ("mod0", leftassoc (fn (t1, t2) => Term.mk_comb (Term.mk_comb
+        (Term.prim_mk_const {Thy="HolSmt", Name="smtmod"}, t1), t2))),
       ("abs", K_zero_one intSyntax.mk_absval),
       ("<=", chainable intSyntax.mk_leq),
       ("<", chainable intSyntax.mk_less),