Bugfix: Create ExcludedMiddle for all Bool terms

In particular we need to add the excluded middle axiom for quantified formulas, so we must not do this in the "instanceof ApplicationTerm" branch.
ultimate-pa · Jun 30, 2020 · cb90e74 · cb90e74
1 parent 2af43a7
commit cb90e74
Show file tree

Hide file tree

Showing 2 changed files with 587 additions and 20 deletions.
diff --git a/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/convert/Clausifier.java b/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/convert/Clausifier.java
@@ -1039,26 +1039,20 @@ public void addTermAxioms(final Term term, final SourceAnnotation source) {
 				}
 
 				final ApplicationTerm at = (ApplicationTerm) term;
-				// Special cases
-				if (term.getSort() == term.getTheory().getBooleanSort()) {
-					if (term != term.getTheory().mTrue && term != term.getTheory().mFalse) {
-						addExcludedMiddleAxiom(term, source);
-					}
-				} else {
-					final FunctionSymbol fs = at.getFunction();
-					if (fs.isIntern()) {
-						if (fs.getName().equals("div")) {
-							addDivideAxioms(at, source);
-						} else if (fs.getName().equals("to_int")) {
-							addToIntAxioms(at, source);
-						} else if (fs.getName().equals("ite") && fs.getReturnSort() != mTheory.getBooleanSort()) {
-							pushOperation(new AddTermITEAxiom(term, source));
-						} else if (fs.getName().equals("store")) {
-							addStoreAxiom(at, source);
-						} else if (fs.getName().equals("@diff")) {
-							addDiffAxiom(at, source);
-							mArrayTheory.notifyDiff((CCAppTerm) ccTerm);
-						}
+				final FunctionSymbol fs = at.getFunction();
+				if (fs.isIntern()) {
+					/* add axioms for certain built-in functions */
+					if (fs.getName().equals("div")) {
+						addDivideAxioms(at, source);
+					} else if (fs.getName().equals("to_int")) {
+						addToIntAxioms(at, source);
+					} else if (fs.getName().equals("ite") && fs.getReturnSort() != mTheory.getBooleanSort()) {
+						pushOperation(new AddTermITEAxiom(term, source));
+					} else if (fs.getName().equals("store")) {
+						addStoreAxiom(at, source);
+					} else if (fs.getName().equals("@diff")) {
+						addDiffAxiom(at, source);
+						mArrayTheory.notifyDiff((CCAppTerm) ccTerm);
 					}
 				}
 
@@ -1084,6 +1078,12 @@ public void addTermAxioms(final Term term, final SourceAnnotation source) {
 					shareLATerm(term, new LASharedTerm(term, mat.getSummands(), mat.getConstant().mReal));
 				}
 			}
+			if (term.getSort() == term.getTheory().getBooleanSort()) {
+				/* If the term is a boolean term, add it's excluded middle axiom */
+				if (term != term.getTheory().mTrue && term != term.getTheory().mFalse) {
+					addExcludedMiddleAxiom(term, source);
+				}
+			}
 		}
 		if (!mIsRunning) {
 			run();