OpenSMT: Add an option to simplify interpolants

Author: daniel-raffler

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java

@@ -82,6 +82,8 @@ static SMTConfig getConfigInstance(
       config.setOption(":interpolation-bool-algorithm", new SMTOption(pSolverOptions.algBool));
       config.setOption(":interpolation-euf-algorithm", new SMTOption(pSolverOptions.algUf));
       config.setOption(":interpolation-lra-algorithm", new SMTOption(pSolverOptions.algLra));
+      config.setOption(
+          ":simplify-interpolants", new SMTOption(pSolverOptions.simplifyInterpolants));
     }
     return config;
   }

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java

@@ -53,6 +53,9 @@ static class OpenSMTOptions {
     @Option(secure = true, description = "Algorithm for LRA interpolation")
     int algLra = 0;
 
+    @Option(secure = true, description = "Simplify interpolants before they are returned")
+    int simplifyInterpolants = 0;
+
     final int randomSeed;
 
     OpenSMTOptions(Configuration config, int pRandomSeed) throws InvalidConfigurationException {