Visitor broken when using OptiMathSAT

[daniel-raffler]

Hello,
while working on this branch I've noticed a failing test for OptiMathSAT here. The exception message reads:

java.lang.UnsatisfiedLinkError: 'boolean org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_is_enum_type(long, long)'
at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_is_enum_type(Native Method)
at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5FormulaCreator.visit(Mathsat5FormulaCreator.java:339)
at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5FormulaCreator.visit(Mathsat5FormulaCreator.java:148)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visit(FormulaCreator.java:296)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visitRecursively(FormulaCreator.java:327)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.visitRecursively(FormulaCreator.java:312)
at org.sosy_lab.java_smt.basicimpl.FormulaCreator.extractVariablesAndUFs(FormulaCreator.java:400)
at org.sosy_lab.java_smt.basicimpl.AbstractModel.asList(AbstractModel.java:40)
at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5Model.<init>(Mathsat5Model.java:37)
at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5AbstractProver.getModel(Mathsat5AbstractProver.java:145)
at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5OptimizationProver.getModel(Mathsat5OptimizationProver.java:153)
at org.sosy_lab.java_smt.test.OptimizationTest.testOptimal(OptimizationTest.java:101)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)

The problem is that the MathSAT visitor code calls msat_is_enum, however, this function seems to be missing from OptiMathSAT. I'm not sure if enums are just not supported by OptiMathSAT or if this is a problem with the way we link the binary. I tried looking up the versions of MathSAT and OptiMathSAT but couldn't find any recent mentions of enums in the release notes. The exception can also be triggered by just calling msat_is_enum_type directly in the native tests, so it's not a problem with just our visitor

We should find out if OptiMathSAT supports enums. If not, we may just have to add some additional checks in the visitor to make sure msat_is_enum is not called when optimization is used