From ebe2dcdeeb60031579143947cd79fe6b4326018b Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Thu, 7 May 2026 18:42:49 +0100 Subject: [PATCH 1/4] examples and changes to use refinements in if conds --- .../AbstractUndoableEditRefinements.java | 29 ++++++++++++++ .../state_test_method_correct/EditCycler.java | 17 +++++++++ .../AbstractUndoableEditRefinements.java | 26 +++++++++++++ .../state_test_method_error/EditMisuse.java | 24 ++++++++++++ .../RefinementTypeChecker.java | 38 +++++++++++++++---- 5 files changed, 127 insertions(+), 7 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/AbstractUndoableEditRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/EditCycler.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/AbstractUndoableEditRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/AbstractUndoableEditRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/AbstractUndoableEditRefinements.java new file mode 100644 index 00000000..35b81156 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/AbstractUndoableEditRefinements.java @@ -0,0 +1,29 @@ +package testSuite.classes.state_test_method_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"aliveDone", "aliveNotDone", "notAlive"}) +@ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit") +public interface AbstractUndoableEditRefinements { + + @StateRefinement(to = "aliveDone(this)") + void AbstractUndoableEdit(); + + @StateRefinement(from = "aliveNotDone(this)", to = "aliveDone(this)") + void redo(); + + @StateRefinement(from = "aliveDone(this)", to = "aliveNotDone(this)") + void undo(); + + @StateRefinement(from = "!notAlive(this)", to = "notAlive(this)") + void die(); + + @Refinement("_ == true --> aliveDone(this)") + boolean canUndo(); + + @Refinement("_ == true --> aliveNotDone(this)") + boolean canRedo(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/EditCycler.java b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/EditCycler.java new file mode 100644 index 00000000..67a4251d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/EditCycler.java @@ -0,0 +1,17 @@ +package testSuite.classes.state_test_method_correct; + +import javax.swing.undo.AbstractUndoableEdit; + +public class EditCycler { + public static void undoIfPossible(AbstractUndoableEdit edit) { + if (edit.canUndo()) { + edit.undo(); + } + } + + public static void redoIfPossible(AbstractUndoableEdit edit) { + if (edit.canRedo()) { + edit.redo(); + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/AbstractUndoableEditRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/AbstractUndoableEditRefinements.java new file mode 100644 index 00000000..a29ba8ac --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/AbstractUndoableEditRefinements.java @@ -0,0 +1,26 @@ +package testSuite.classes.state_test_method_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"aliveDone", "aliveNotDone", "notAlive"}) +@ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit") +public interface AbstractUndoableEditRefinements { + + @StateRefinement(to = "aliveDone(this)") + void AbstractUndoableEdit(); + + @StateRefinement(from = "aliveNotDone(this)", to = "aliveDone(this)") + void redo(); + + @StateRefinement(from = "aliveDone(this)", to = "aliveNotDone(this)") + void undo(); + + @Refinement("_ == true --> aliveDone(this)") + boolean canUndo(); + + @Refinement("_ == true --> aliveNotDone(this)") + boolean canRedo(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java new file mode 100644 index 00000000..79163df3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java @@ -0,0 +1,24 @@ +package testSuite.classes.state_test_method_error; + +import javax.swing.undo.AbstractUndoableEdit; + +public class EditMisuse { + + public static void undoInElseBranch(AbstractUndoableEdit edit) { + if (edit.canUndo()) { + } else { + edit.undo(); // State Refinement Error + } + } + + public static void undoNotInElse(AbstractUndoableEdit edit) { + if (!edit.canUndo()) { + edit.undo(); // State Refinement Error + } + } + public static void wrongTesterForRedo(AbstractUndoableEdit edit) { + if (edit.canUndo()) { + edit.redo(); // State Refinement Error + } + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 50ba05f5..d6706d03 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -343,24 +343,47 @@ public void visitCtIf(CtIf ifElement) { String pathVarName = String.format(Formats.FRESH, context.getCounter()); RefinedVariable freshRV; + // The condition's predicate may use Keys.WILDCARD as a stand-in for the boolean value of the condition + // (e.g. invocation post-conditions of the form `_ == true --> state(this)`, or variable reads `_ == k`). + // When that's the case the fresh path variable IS that boolean value, so we assert it true in the then + // branch and false in the else branch — instead of negating the whole predicate, which is unsound for + // implications and equality forms. + boolean valueIsCondition = false; + Predicate thenRefs; + Predicate elseRefs; if (isUninformativeCondition(expRefs, exp)) { // No refinement means the condition is unknown, not true: model it as a fresh // boolean so the SMT solver may pick either truth value for each branch. expRefs = Predicate.createVar(pathVarName); + thenRefs = expRefs; + elseRefs = expRefs.negate(); freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, new Predicate(), exp); } else { + valueIsCondition = expRefs.getVariableNames().contains(Keys.WILDCARD); expRefs = expRefs.substituteVariable(Keys.WILDCARD, pathVarName); Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs); expRefs = Predicate.createConjunction(expRefs, lastExpRefs); - freshRV = context.addInstanceToContext(pathVarName, factory.Type().INTEGER_PRIMITIVE, expRefs, exp); - } + // TODO Change in future + if (expRefs.getVariableNames().contains("null")) { + expRefs = new Predicate(); + valueIsCondition = false; + } - // TODO Change in future - if (expRefs.getVariableNames().contains("null")) { - expRefs = new Predicate(); + thenRefs = expRefs; + elseRefs = expRefs.negate(); + if (valueIsCondition) { + Predicate freshIsTrue = Predicate.createEquals(Predicate.createVar(pathVarName), + Predicate.createLit("true", Types.BOOLEAN)); + Predicate freshIsFalse = Predicate.createEquals(Predicate.createVar(pathVarName), + Predicate.createLit("false", Types.BOOLEAN)); + thenRefs = Predicate.createConjunction(expRefs, freshIsTrue); + elseRefs = Predicate.createConjunction(expRefs, freshIsFalse); + freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp); + } else { + freshRV = context.addInstanceToContext(pathVarName, factory.Type().INTEGER_PRIMITIVE, expRefs, exp); + } } - vcChecker.addPathVariable(freshRV); context.variablesNewIfCombination(); @@ -378,7 +401,8 @@ public void visitCtIf(CtIf ifElement) { // VISIT ELSE if (ifElement.getElseStatement() != null) { - context.newRefinementToVariableInContext(pathVarName, expRefs.negate()); + context.getVariableByName(pathVarName); + context.newRefinementToVariableInContext(pathVarName, elseRefs); context.enterContext(); visitCtBlock(ifElement.getElseStatement()); From be54bb0413e9a621139b7d164f7d005b3018e294 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 8 May 2026 12:13:46 +0100 Subject: [PATCH 2/4] one more example --- .../classes/state_test_method_error/EditMisuse.java | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java index 79163df3..f45e056a 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java +++ b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java @@ -21,4 +21,14 @@ public static void wrongTesterForRedo(AbstractUndoableEdit edit) { edit.redo(); // State Refinement Error } } + + public static void wrongTester2() { + AbstractUndoableEdit edit = new AbstractUndoableEdit(); + edit.undo(); // edit: aliveNotDone + if (edit.canUndo()) { // is canUndo() == true --> edit: aliveDone + edit.undo(); // edit: aliveNotDone + } + edit.undo(); // is "aliveDone(this)"? not in any path + + } } From f77ef6b1c4ee4962ea22a455aa0c73916c9f0785 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 8 May 2026 16:50:59 +0100 Subject: [PATCH 3/4] add iterator and more examples --- .../IteratorRefinements.java | 25 +++++++ .../IteratorUse.java | 36 +++++++++ .../IteratorMisuse.java | 62 +++++++++++++++ .../IteratorRefinements.java | 25 +++++++ .../state_test_method_correct/EditCycler.java | 6 ++ .../state_test_method_error/EditMisuse.java | 75 +++++++++++++++++-- .../RefinementTypeChecker.java | 3 + 7 files changed, 225 insertions(+), 7 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/iterator_observer_correct/IteratorRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/iterator_observer_correct/IteratorUse.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorMisuse.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorRefinements.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_correct/IteratorRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_correct/IteratorRefinements.java new file mode 100644 index 00000000..733e8b86 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_correct/IteratorRefinements.java @@ -0,0 +1,25 @@ +package testSuite.classes.iterator_observer_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +/** + * Observer-style iteration over {@link java.util.Scanner} (an iterator-shaped JDK class): + * {@code hasNext} is an informative check (no state change), and {@code next} consumes one + * element, resetting state so a fresh check is required before the next consumption. + * + *

{@code java.util.Iterator} itself is an interface, and external refinements only attach to + * classes — Scanner gives us the same API in a class form. + */ +@StateSet({"hasMore", "noMore"}) +@ExternalRefinementsFor("java.util.Scanner") +public interface IteratorRefinements { + + @Refinement("_ == true --> hasMore(this)") + boolean hasNext(); + + @StateRefinement(from = "hasMore(this)", to = "noMore(this)") + String next(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_correct/IteratorUse.java b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_correct/IteratorUse.java new file mode 100644 index 00000000..9a3be805 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_correct/IteratorUse.java @@ -0,0 +1,36 @@ +package testSuite.classes.iterator_observer_correct; + +import java.util.Scanner; + +public class IteratorUse { + + public static void readOne(Scanner it) { + if (it.hasNext()) { + it.next(); + } + } + + public static void readTwo(Scanner it) { + if (it.hasNext()) { + it.next(); + if (it.hasNext()) { + it.next(); + } + } + } + + public static void readInElse(Scanner it) { + if (!it.hasNext()) { + } else { + it.next(); + } + } + + public static void recursive(Scanner it) { + if (it.hasNext()) { + String s = it.next(); + System.out.println(s); + recursive(it); + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorMisuse.java b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorMisuse.java new file mode 100644 index 00000000..4aa1f52b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorMisuse.java @@ -0,0 +1,62 @@ +package testSuite.classes.iterator_observer_error; + +import java.util.Scanner; + +public class IteratorMisuse { + + // No check at all: state of the parameter is unknown. + public static void nextWithoutCheck(Scanner it) { + it.next(); // State Refinement Error + } + + // Else branch of hasNext(): condition was false, so we know !hasMore. + public static void nextInElseBranch(Scanner it) { + if (it.hasNext()) { + } else { + it.next(); // State Refinement Error + } + } + + // Negated check: !hasNext() true means hasNext returned false, so !hasMore. + public static void nextNotInElse(Scanner it) { + if (!it.hasNext()) { + it.next(); // State Refinement Error + } + } + + // After consuming with next(), state becomes noMore — a second next() in the same + // then-branch must fail. + public static void doubleNextInThen(Scanner it) { + if (it.hasNext()) { + it.next(); + it.next(); // State Refinement Error + } + } + + // Empty if-then: the bug we fixed in visitCtIf would have masked this join, leaking the + // path-variable's truthiness past the if and silently asserting hasMore. + public static void nextAfterEmptyIf(Scanner it) { + if (it.hasNext()) { + } + it.next(); // State Refinement Error + } + + // Sequential ifs: state is consumed by the first then-branch's next(), and the second if's + // path-variable assertion must not leak past its join. + public static void sequentialIfsLoseState(Scanner it) { + if (it.hasNext()) { + it.next(); + } + if (it.hasNext()) { + } + it.next(); // State Refinement Error + } + + // Empty if + empty else: neither branch establishes hasMore. + public static void nextAfterEmptyIfElse(Scanner it) { + if (it.hasNext()) { + } else { + } + it.next(); // State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorRefinements.java new file mode 100644 index 00000000..7574607a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_observer_error/IteratorRefinements.java @@ -0,0 +1,25 @@ +package testSuite.classes.iterator_observer_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Refinement; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +/** + * Observer-style iteration over {@link java.util.Scanner} (an iterator-shaped JDK class): + * {@code hasNext} is an informative check (no state change), and {@code next} consumes one + * element, resetting state so a fresh check is required before the next consumption. + * + *

{@code java.util.Iterator} itself is an interface, and external refinements only attach to + * classes — Scanner gives us the same API in a class form. + */ +@StateSet({"hasMore", "noMore"}) +@ExternalRefinementsFor("java.util.Scanner") +public interface IteratorRefinements { + + @Refinement("_ == true --> hasMore(this)") + boolean hasNext(); + + @StateRefinement(from = "hasMore(this)", to = "noMore(this)") + String next(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/EditCycler.java b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/EditCycler.java index 67a4251d..63383cc2 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/EditCycler.java +++ b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_correct/EditCycler.java @@ -14,4 +14,10 @@ public static void redoIfPossible(AbstractUndoableEdit edit) { edit.redo(); } } + + public static void redoIfPossible() { + AbstractUndoableEdit edit = new AbstractUndoableEdit(); + edit.canRedo(); + edit.undo(); + } } diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java index f45e056a..236437bf 100644 --- a/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java +++ b/liquidjava-example/src/main/java/testSuite/classes/state_test_method_error/EditMisuse.java @@ -14,21 +14,82 @@ public static void undoInElseBranch(AbstractUndoableEdit edit) { public static void undoNotInElse(AbstractUndoableEdit edit) { if (!edit.canUndo()) { edit.undo(); // State Refinement Error - } + } } + public static void wrongTesterForRedo(AbstractUndoableEdit edit) { if (edit.canUndo()) { edit.redo(); // State Refinement Error } } - public static void wrongTester2() { + public static void wrongTester2() { + AbstractUndoableEdit edit = new AbstractUndoableEdit(); + edit.undo(); + if (edit.canUndo()) { + edit.undo(); + } + edit.undo(); // State Refinement Error + } + + // Two undos in the same then-branch: condition forces aliveDone for the first, but the second + // is in aliveNotDone. + public static void doubleUndoInThen(AbstractUndoableEdit edit) { + if (edit.canUndo()) { + edit.undo(); + edit.undo(); // State Refinement Error + } + } + + // Nested ifs: outer canUndo => aliveDone, inner canUndo => aliveDone (still), so calling + // redo() in the inner then is illegal (redo needs aliveNotDone). + public static void nestedIfRedoFromAliveDone(AbstractUndoableEdit edit) { + if (edit.canUndo()) { + if (edit.canUndo()) { + edit.redo(); // State Refinement Error + } + } + } + + // Sequential guarded undos with no else: after the first if, state is aliveNotDone in BOTH + // paths (then took canUndo=>aliveDone then undo=>aliveNotDone; else had canUndo=false meaning + // !aliveDone, which can only be aliveNotDone given the state set). The second undo therefore + // cannot succeed — but the verifier must not let the first if's truth assertion leak. + public static void sequentialIfsLoseState() { + AbstractUndoableEdit edit = new AbstractUndoableEdit(); + if (edit.canUndo()) { + edit.undo(); + } + if (edit.canUndo()) { + } + edit.undo(); // State Refinement Error + } + + // Wrong direction: canRedo() implies aliveNotDone, so calling undo() in that branch is illegal. + public static void undoGuardedByCanRedo(AbstractUndoableEdit edit) { + if (edit.canRedo()) { + edit.undo(); // State Refinement Error + } + } + + // Redo after undo inside the then: the inner state is aliveDone -> aliveNotDone -> aliveDone + // after redo, so a second redo from aliveDone is illegal. + public static void doubleRedoAfterUndo(AbstractUndoableEdit edit) { + if (edit.canUndo()) { + edit.undo(); + edit.redo(); + edit.redo(); // State Refinement Error + } + } + + // Empty if / empty else: the bug we fixed would have let `pathVar == true` (or false) leak past + // the join, masking violations. Here the constructor leaves edit in aliveDone, neither branch + // changes it, so after the if the state is still aliveDone — calling redo() is illegal. + public static void redoAfterEmptyIfElse() { AbstractUndoableEdit edit = new AbstractUndoableEdit(); - edit.undo(); // edit: aliveNotDone - if (edit.canUndo()) { // is canUndo() == true --> edit: aliveDone - edit.undo(); // edit: aliveNotDone + if (edit.canUndo()) { + } else { } - edit.undo(); // is "aliveDone(this)"? not in any path - + edit.redo(); // State Refinement Error } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index d6706d03..d8613796 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -413,6 +413,9 @@ public void visitCtIf(CtIf ifElement) { context.exitContext(); } // end + // Reset the path variable's refinement to the original condition after the if, + // so branch-local truth assertions (and any typestate they imply) don't leak past the join. + context.newRefinementToVariableInContext(pathVarName, expRefs); vcChecker.removePathVariable(freshRV); context.exitContext(); context.variablesCombineFromIf(expRefs); From e705514f92b6a44bef348813bcb9d2702d79da65 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Fri, 8 May 2026 17:34:18 +0100 Subject: [PATCH 4/4] small cleanup --- .../refinement_checker/RefinementTypeChecker.java | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index d8613796..09095f35 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -343,11 +343,10 @@ public void visitCtIf(CtIf ifElement) { String pathVarName = String.format(Formats.FRESH, context.getCounter()); RefinedVariable freshRV; - // The condition's predicate may use Keys.WILDCARD as a stand-in for the boolean value of the condition - // (e.g. invocation post-conditions of the form `_ == true --> state(this)`, or variable reads `_ == k`). - // When that's the case the fresh path variable IS that boolean value, so we assert it true in the then - // branch and false in the else branch — instead of negating the whole predicate, which is unsound for - // implications and equality forms. + + // When the condition's predicate uses Keys.WILDCARD as a stand-in for its boolean value (e.g. _ == true --> + // state(this) or _ == k), the fresh path variable IS that value — assert it true in the then branch and false + // in the else, since negating the whole predicate is unsound for implications and equality forms. boolean valueIsCondition = false; Predicate thenRefs; Predicate elseRefs; @@ -379,10 +378,9 @@ public void visitCtIf(CtIf ifElement) { Predicate.createLit("false", Types.BOOLEAN)); thenRefs = Predicate.createConjunction(expRefs, freshIsTrue); elseRefs = Predicate.createConjunction(expRefs, freshIsFalse); - freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp); - } else { - freshRV = context.addInstanceToContext(pathVarName, factory.Type().INTEGER_PRIMITIVE, expRefs, exp); } + + freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp); } vcChecker.addPathVariable(freshRV);