From 68539cbe6106cb738eee2cdb76c49c5a3ca483c6 Mon Sep 17 00:00:00 2001
From: Alexander Nutz <nutz@informatik.uni-freiburg.de>
Date: Mon, 7 Aug 2017 10:22:48 +0200
Subject: [PATCH] bugfixes, #143

---
 .../treeautomizer/graph/HCSSABuilder.java     | 23 +++++++++++++++----
 1 file changed, 19 insertions(+), 4 deletions(-)

diff --git a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSSABuilder.java b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSSABuilder.java
index 1d9d095be57..67ac1efdf90 100644
--- a/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSSABuilder.java
+++ b/trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/HCSSABuilder.java
@@ -140,6 +140,10 @@ public TreeRun<HornClause, IPredicate> buildTreeRunWithBackVersionedInterpolants
 	private TreeRun<HornClause, IPredicate> buildBackVersionedTreeRunRec(TreeRun<HornClause, IPredicate> currentSubTree,
 			Map<TreeRun<HornClause, IPredicate>, Term> interpolantsMap) {
 		final TreeRun<HornClause, SsaInfo> currentSsaSubtree = mInputSubTreeToSsaSubtree.get(currentSubTree);
+		if (currentSsaSubtree == null) {
+			// we're at a leaf
+			return new TreeRun<>(mPredicateUnifier.getTruePredicate());
+		}
 		final Term currentInterpolantTermInSsa = interpolantsMap.get(currentSubTree);
 		final HornClause currentHornClause = currentSubTree.getRootSymbol();
 
@@ -193,12 +197,12 @@ private TreeRun<HornClause, SsaInfo> buildSSArec(TreeRun<HornClause, IPredicate>
 			subTreeRuns.add(subTreeRun);
 		}
 
-		final TreeRun<HornClause, SsaInfo> res;
 		if (subTreeRuns.isEmpty()) {
-			res = new TreeRun<>(ssaInfo);
-		} else {
-			res = new TreeRun<>(ssaInfo, currentHornClause, subTreeRuns);
+			subTreeRuns.add(new TreeRun<>(new SsaInfo()));
 		}
+			
+		final TreeRun<HornClause, SsaInfo> res;
+			res = new TreeRun<>(ssaInfo, currentHornClause, subTreeRuns);
 		mInputSubTreeToSsaSubtree.put(inputTreeRun, res);
 
 		return res;
@@ -273,6 +277,17 @@ class SsaInfo {
 	final Map<Term, Term> mBackSubstitution;
 	final Term mSsaFormula;
 	final List<List<ApplicationTerm>> mSubstitutionForBodyPred;
+	
+	/**
+	 * constructs an empty SSaInfo (its fields should not be accessed..
+	 */
+	public SsaInfo() {
+		mHornClause = null;
+		mSubstitution = null;
+		mBackSubstitution = null;
+		mSsaFormula = null;
+		mSubstitutionForBodyPred = null;
+	}
 
 	/**
 	 *