diff --git a/plugins/org.eclipse.ocl.pivot/.settings/.api_filters b/plugins/org.eclipse.ocl.pivot/.settings/.api_filters
index 829cb6c..8c45f42 100644
--- a/plugins/org.eclipse.ocl.pivot/.settings/.api_filters
+++ b/plugins/org.eclipse.ocl.pivot/.settings/.api_filters
@@ -316,6 +316,18 @@
                 <message_argument value="getTypeId2()"/>
             </message_arguments>
         </filter>
+        <filter id="404000815">
+            <message_arguments>
+                <message_argument value="org.eclipse.ocl.pivot.values.Value"/>
+                <message_argument value="mayBeInvalid()"/>
+            </message_arguments>
+        </filter>
+        <filter id="404000815">
+            <message_arguments>
+                <message_argument value="org.eclipse.ocl.pivot.values.Value"/>
+                <message_argument value="mayBeNull()"/>
+            </message_arguments>
+        </filter>
     </resource>
     <resource path="emf-gen/org/eclipse/ocl/pivot/values/ValuesPackage.java" type="org.eclipse.ocl.pivot.values.ValuesPackage">
         <filter id="403804204">
@@ -767,6 +779,14 @@
             </message_arguments>
         </filter>
     </resource>
+    <resource path="src/org/eclipse/ocl/pivot/internal/manager/MetamodelManagerInternal.java" type="org.eclipse.ocl.pivot.internal.manager.MetamodelManagerInternal$MetamodelManagerInternalExtension2">
+        <filter id="404000815">
+            <message_arguments>
+                <message_argument value="org.eclipse.ocl.pivot.internal.manager.MetamodelManagerInternal.MetamodelManagerInternalExtension2"/>
+                <message_argument value="getSymbolicAnalysis(ExpressionInOCL, Object, Object[])"/>
+            </message_arguments>
+        </filter>
+    </resource>
     <resource path="src/org/eclipse/ocl/pivot/internal/resource/ASResourceFactory.java" type="org.eclipse.ocl.pivot.internal.resource.ASResourceFactory">
         <filter id="404000815">
             <message_arguments>
@@ -813,6 +833,14 @@
             </message_arguments>
         </filter>
     </resource>
+    <resource path="src/org/eclipse/ocl/pivot/library/oclany/OclAnyToStringOperation.java" type="org.eclipse.ocl.pivot.library.oclany.OclAnyToStringOperation">
+        <filter id="336658481">
+            <message_arguments>
+                <message_argument value="org.eclipse.ocl.pivot.library.oclany.OclAnyToStringOperation"/>
+                <message_argument value="INSTANCE2"/>
+            </message_arguments>
+        </filter>
+    </resource>
     <resource path="src/org/eclipse/ocl/pivot/resource/BasicProjectManager.java" type="org.eclipse.ocl.pivot.resource.BasicProjectManager">
         <filter comment="Bug 512402 workaround" id="576725006">
             <message_arguments>
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/CollectionValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/CollectionValueImpl.java
index a2156b6..4a9cc79 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/CollectionValueImpl.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/CollectionValueImpl.java
@@ -719,13 +719,6 @@
 	}
 
 	@Override
-	public String toString() {
-		StringBuilder s = new StringBuilder();
-		toString(s, 100);
-		return s.toString();
-	}
-
-	@Override
 	public void toString(@NonNull StringBuilder s, int lengthLimit) {
 		s.append("{");
 		boolean isFirst = true;
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/MapValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/MapValueImpl.java
index fe342ae..2624199 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/MapValueImpl.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/MapValueImpl.java
@@ -572,13 +572,6 @@
 	}
 
 	@Override
-	public String toString() {
-		StringBuilder s = new StringBuilder();
-		toString(s, 100);
-		return s.toString();
-	}
-
-	@Override
 	public void toString(@NonNull StringBuilder s, int lengthLimit) {
 		s.append(TypeId.MAP_NAME);
 		s.append("{");
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/NullValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/NullValueImpl.java
index 6a39a08..b71f0c9 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/NullValueImpl.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/NullValueImpl.java
@@ -131,11 +131,30 @@
 		return false;
 	}
 
+	/**
+	 * @since 1.12
+	 */
+	@Override
+	public boolean mayBeInvalid() {
+		return false;
+	}
+
+	/**
+	 * @since 1.12
+	 */
+	@Override
+	public boolean mayBeNull() {
+		return true;
+	}
+
 	@Override
 	public boolean oclEquals(@NonNull OCLValue thatValue) {
 		return equals(thatValue);
 	}
 
+	/**
+	 * @since 1.12
+	 */
 	@Override
 	public int oclHashCode() {
 		return hashCode();
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/NumberValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/NumberValueImpl.java
index 2e53c13..c4eca6f 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/NumberValueImpl.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/NumberValueImpl.java
@@ -241,6 +241,22 @@
 		return false;
 	}
 
+	/**
+	 * @since 1.12
+	 */
+	@Override
+	public boolean mayBeInvalid() {
+		return false;
+	}
+
+	/**
+	 * @since 1.12
+	 */
+	@Override
+	public boolean mayBeNull() {
+		return false;
+	}
+
 	@Override
 	public boolean oclEquals(@NonNull OCLValue thatValue) {
 		return equals(thatValue);
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/ObjectValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/ObjectValueImpl.java
index 5957a66..2b41735 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/ObjectValueImpl.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/ObjectValueImpl.java
@@ -78,7 +78,7 @@
 	}
 
 	@Override
-	public String toString() {
-		return String.valueOf(getObject());
+	public void toString(@NonNull StringBuilder s, int lengthLimit) {
+		s.append(String.valueOf(getObject()));
 	}
 } //ObjectValueImpl
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicNavigationCallValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicNavigationCallValueImpl.java
new file mode 100644
index 0000000..b383066
--- /dev/null
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicNavigationCallValueImpl.java
@@ -0,0 +1,73 @@
+/**
+ * Copyright (c) 2010, 2020 Willink Transformations and others.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v2.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v20.html
+ *
+ * Contributors:
+ *   E.D.Willink - Initial API and implementation
+ */
+package org.eclipse.ocl.pivot.internal.values;
+
+import org.eclipse.jdt.annotation.NonNull;
+import org.eclipse.jdt.annotation.Nullable;
+import org.eclipse.ocl.pivot.NavigationCallExp;
+import org.eclipse.ocl.pivot.ids.TypeId;
+import org.eclipse.ocl.pivot.utilities.PivotUtil;
+import org.eclipse.ocl.pivot.values.Value;
+
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>Symbolic Value</b></em>'.
+ * @since 1.12
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class SymbolicNavigationCallValueImpl extends SymbolicValueImpl {
+
+	protected final @NonNull NavigationCallExp navigationCallExp;
+	protected final @Nullable Object sourceValue;
+//	protected final @NonNull Property property;
+
+		/**
+	 * <!-- begin-user-doc -->
+	 * <!-- end-user-doc -->
+	 * @param variable
+	 * @generated NOT
+	 */
+	public SymbolicNavigationCallValueImpl(@NonNull NavigationCallExp navigationCallExp, @Nullable Object sourceValue) {//, @NonNull Property property) {
+		this.navigationCallExp = navigationCallExp;
+		this.sourceValue = sourceValue;
+//		this.property = property;
+	}
+
+//	@Override
+//	public @NonNull EObject asNavigableObject() {
+//		return this;
+//	}
+
+	@Override
+	public @NonNull TypeId getTypeId() {
+		return navigationCallExp.getTypeId();
+	}
+
+	@Override
+	public boolean mayBeNull() {
+		return !navigationCallExp.isIsRequired();
+	}
+
+	@Override
+	public void toString(@NonNull StringBuilder s, int lengthLimit) {
+		if (sourceValue instanceof Value){
+			((Value)sourceValue).toString(s, lengthLimit);
+		}
+		else {
+			s.append(String.valueOf(sourceValue));
+		}
+		s.append(".");
+		s.append(PivotUtil.getReferredProperty(navigationCallExp).getName());
+	}
+
+} //SymbolicValueImpl
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicStringValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicStringValueImpl.java
new file mode 100644
index 0000000..a8fcbdb
--- /dev/null
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicStringValueImpl.java
@@ -0,0 +1,149 @@
+/**
+ * Copyright (c) 2010, 2020 Willink Transformations and others.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v2.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v20.html
+ *
+ * Contributors:
+ *   E.D.Willink - Initial API and implementation
+ */
+package org.eclipse.ocl.pivot.internal.values;
+
+import org.eclipse.jdt.annotation.NonNull;
+import org.eclipse.jdt.annotation.Nullable;
+import org.eclipse.ocl.pivot.ids.TypeId;
+
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>Symbolic Value</b></em>'.
+ * @since 1.12
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class SymbolicStringValueImpl extends SymbolicValueImpl { //implements EObject {
+
+	protected final @Nullable Object sourceValue;
+	/**
+	 * <!-- begin-user-doc -->
+	 * <!-- end-user-doc -->
+	 * @param variable
+	 * @generated NOT
+	 */
+	public SymbolicStringValueImpl(@Nullable Object sourceValue) {
+		this.sourceValue = sourceValue;
+	}
+
+//	@Override
+//	public @NonNull EObject asNavigableObject() {
+//		return this;
+//	}
+
+	@Override
+	public @NonNull TypeId getTypeId() {
+		return TypeId.STRING;
+	}
+
+	@Override
+	public void toString(@NonNull StringBuilder s, int lengthLimit) {
+		s.append("'");
+		s.append(String.valueOf(sourceValue));
+		s.append("'");
+	}
+
+/*	@Override
+	public EList<Adapter> eAdapters() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public boolean eDeliver() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void eSetDeliver(boolean deliver) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void eNotify(Notification notification) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public EClass eClass() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public Resource eResource() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public EObject eContainer() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public EStructuralFeature eContainingFeature() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public EReference eContainmentFeature() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public EList<EObject> eContents() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public TreeIterator<@NonNull EObject> eAllContents() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public boolean eIsProxy() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public EList<EObject> eCrossReferences() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public Object eGet(EStructuralFeature feature) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public Object eGet(EStructuralFeature feature, boolean resolve) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void eSet(EStructuralFeature feature, Object newValue) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public boolean eIsSet(EStructuralFeature feature) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void eUnset(EStructuralFeature feature) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public Object eInvoke(EOperation operation, EList<?> arguments) throws InvocationTargetException {
+		throw new UnsupportedOperationException();
+	} */
+} //SymbolicValueImpl
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicUnknownValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicUnknownValueImpl.java
new file mode 100644
index 0000000..d05a896
--- /dev/null
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicUnknownValueImpl.java
@@ -0,0 +1,169 @@
+/**
+ * Copyright (c) 2010, 2020 Willink Transformations and others.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v2.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v20.html
+ *
+ * Contributors:
+ *   E.D.Willink - Initial API and implementation
+ */
+package org.eclipse.ocl.pivot.internal.values;
+
+import java.util.List;
+
+import org.eclipse.jdt.annotation.NonNull;
+import org.eclipse.jdt.annotation.Nullable;
+import org.eclipse.ocl.pivot.Element;
+import org.eclipse.ocl.pivot.ids.CollectionTypeId;
+import org.eclipse.ocl.pivot.ids.IdResolver;
+import org.eclipse.ocl.pivot.ids.OclVoidTypeId;
+import org.eclipse.ocl.pivot.ids.TupleTypeId;
+import org.eclipse.ocl.pivot.ids.TypeId;
+import org.eclipse.ocl.pivot.messages.PivotMessages;
+import org.eclipse.ocl.pivot.values.InvalidValueException;
+import org.eclipse.ocl.pivot.values.NullValue;
+import org.eclipse.ocl.pivot.values.OCLValue;
+import org.eclipse.ocl.pivot.values.RealValue;
+import org.eclipse.ocl.pivot.values.SymbolicValue;
+
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>Symbolic Value</b></em>'.
+ * @since 1.12
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class SymbolicUnknownValueImpl extends UndefinedValueImpl implements SymbolicValue {
+	private static final long serialVersionUID = 1L;
+
+	protected final @NonNull TypeId typeId;
+	protected final boolean mayBeNull;
+	protected final boolean mayBeInvalid;
+	/**
+	 * <!-- begin-user-doc -->
+	 * <!-- end-user-doc -->
+	 * @param variable
+	 * @generated NOT
+	 */
+	public SymbolicUnknownValueImpl(@NonNull TypeId typeId, boolean mayBeNull, boolean mayBeInvalid) {
+		super("dummy-message");
+		this.typeId = typeId;
+		this.mayBeNull = mayBeNull;
+		this.mayBeInvalid = mayBeInvalid;
+	}
+
+//	@Override
+//	public @NonNull EObject asNavigableObject() {
+//		return this;
+//	}
+
+	@Override
+	public @NonNull NullValue divideReal(@NonNull RealValue right) {
+		if (right.asDouble() == 1.0) {
+			return this;
+		}
+	//	double x = 1/0 / 0.0;
+		if (right.asDouble() == 0.0) {
+			throw new InvalidValueException(new ArithmeticException("/ by zero"));
+		}
+		return this;
+	}
+
+	@Override
+	public @NonNull CollectionTypeId getCollectionTypeId() {
+		throw new InvalidValueException(PivotMessages.ConvertibleValueRequired, "Invalid");
+	}
+
+	@Override
+	public @NonNull RealValue asRealValue() {
+		if (typeId == TypeId.REAL) {
+			return this;
+		}
+		return super.asRealValue();
+	}
+
+	@Override
+	public @NonNull TupleTypeId getTupleTypeId() {
+		throw new InvalidValueException(PivotMessages.ConvertibleValueRequired, "Invalid");
+	}
+
+	@Override
+	public @NonNull OclVoidTypeId getTypeId() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public @NonNull TypeId getTypeId2() {
+		return typeId;
+	}
+
+	@Override
+	public boolean mayBeInvalid() {
+		return mayBeInvalid;
+	}
+
+	@Override
+	public boolean mayBeNull() {
+		return mayBeNull;
+	}
+
+	@Override
+	public void toString(@NonNull StringBuilder s, int lengthLimit) {
+		s.append(typeId);
+		s.append("-");
+		s.append(mayBeNull);
+		s.append("-");
+		s.append(mayBeInvalid);
+	}
+
+	@Override
+	public Element asElement() {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	@Override
+	public Object asUnboxedObject(@NonNull IdResolver idResolver) {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	@Override
+	public boolean isInvalid() {
+		// TODO Auto-generated method stub
+		return false;
+	}
+
+//	@Override
+//	public @NonNull OclVoidTypeId getTypeId() {
+		// TODO Auto-generated method stub
+//		return null;
+//	}
+
+	@Override
+	public int intValue() {
+		// TODO Auto-generated method stub
+		return 0;
+	}
+
+	@Override
+	public boolean oclEquals(@NonNull OCLValue thatValue) {
+		// TODO Auto-generated method stub
+		return false;
+	}
+
+	@Override
+	public int oclHashCode() {
+		// TODO Auto-generated method stub
+		return 0;
+	}
+
+	@Override
+	public @Nullable List<?> asEcoreObject(@NonNull IdResolver idResolver,
+			@Nullable Class<?> instanceClass) {
+		// TODO Auto-generated method stub
+		return null;
+	}
+} //SymbolicValueImpl
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicValueImpl.java
index a20758b..6ef8ad2 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicValueImpl.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicValueImpl.java
@@ -60,7 +60,7 @@
 
 	@Override
 	public @NonNull TypeId getTypeId() {
-		throw new UnsupportedOperationException();
+		return getTypeId2();
 	}
 
 	@Override
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicVariableValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicVariableValueImpl.java
new file mode 100644
index 0000000..0398a4e
--- /dev/null
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicVariableValueImpl.java
@@ -0,0 +1,152 @@
+/**
+ * Copyright (c) 2010, 2020 Willink Transformations and others.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v2.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v20.html
+ *
+ * Contributors:
+ *   E.D.Willink - Initial API and implementation
+ */
+package org.eclipse.ocl.pivot.internal.values;
+
+import org.eclipse.jdt.annotation.NonNull;
+import org.eclipse.ocl.pivot.VariableDeclaration;
+import org.eclipse.ocl.pivot.ids.TypeId;
+
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>Symbolic Value</b></em>'.
+ * @since 1.12
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class SymbolicVariableValueImpl extends SymbolicValueImpl { //implements EObject {
+
+	protected final @NonNull VariableDeclaration variable;
+	/**
+	 * <!-- begin-user-doc -->
+	 * <!-- end-user-doc -->
+	 * @param variable
+	 * @generated NOT
+	 */
+	public SymbolicVariableValueImpl(@NonNull VariableDeclaration variable) {
+		this.variable = variable;
+	}
+
+//	@Override
+//	public @NonNull EObject asNavigableObject() {
+//		return this;
+//	}
+
+	@Override
+	public @NonNull TypeId getTypeId() {
+		return variable.getTypeId();
+	}
+
+	@Override
+	public boolean mayBeNull() {
+		return !variable.isIsRequired();
+	}
+
+	@Override
+	public void toString(@NonNull StringBuilder s, int lengthLimit) {
+		s.append(variable.getName());
+	}
+
+/*	@Override
+	public EList<Adapter> eAdapters() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public boolean eDeliver() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void eSetDeliver(boolean deliver) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void eNotify(Notification notification) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public EClass eClass() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public Resource eResource() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public EObject eContainer() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public EStructuralFeature eContainingFeature() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public EReference eContainmentFeature() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public EList<EObject> eContents() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public TreeIterator<@NonNull EObject> eAllContents() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public boolean eIsProxy() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public EList<EObject> eCrossReferences() {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public Object eGet(EStructuralFeature feature) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public Object eGet(EStructuralFeature feature, boolean resolve) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void eSet(EStructuralFeature feature, Object newValue) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public boolean eIsSet(EStructuralFeature feature) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public void eUnset(EStructuralFeature feature) {
+		throw new UnsupportedOperationException();
+	}
+
+	@Override
+	public Object eInvoke(EOperation operation, EList<?> arguments) throws InvocationTargetException {
+		throw new UnsupportedOperationException();
+	} */
+} //SymbolicValueImpl
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/ValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/ValueImpl.java
index 233be84..beaf0f4 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/ValueImpl.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/ValueImpl.java
@@ -273,6 +273,23 @@
 		return false;
 	}
 
+	@Override
+	public boolean mayBeInvalid() {
+		return false;
+	}
+
+	@Override
+	public boolean mayBeNull() {
+		return false;
+	}
+
+	@Override
+	public /*final*/ @NonNull String toString() {
+		StringBuilder s = new StringBuilder();
+		toString(s, 100);
+		return s.toString();
+	}
+
 	/**
 	 * @generated NOT
 	 */
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/CollectionValue.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/CollectionValue.java
index 0db02da..a58a222 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/CollectionValue.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/CollectionValue.java
@@ -91,17 +91,18 @@
 
 	/**
 	 * @generated NOT
+	 */
+	boolean flatten(@NonNull Collection<Object> flattenedElements);
+
+	/**
+	 * @generated NOT
 	 * @since 1.12
 	 */
 	default @NonNull CollectionTypeId getCollectionTypeId() { return getTypeId(); }
 
 	/**
 	 * @generated NOT
-	 */
-	boolean flatten(@NonNull Collection<Object> flattenedElements);
-
-	/**
-	 * @generated NOT
+	 * @since 1.12
 	 */
 	@NonNull Collection<? extends Object> getElements();
 
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/InvalidValueException.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/InvalidValueException.java
index af63cf5..9aad8ef 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/InvalidValueException.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/InvalidValueException.java
@@ -219,6 +219,22 @@
 		return true;
 	}
 
+	/**
+	 * @since 1.12
+	 */
+	@Override
+	public boolean mayBeInvalid() {
+		return true;
+	}
+
+	/**
+	 * @since 1.12
+	 */
+	@Override
+	public boolean mayBeNull() {
+		return false;
+	}
+
 	@Override
 	public boolean oclEquals(@NonNull OCLValue thatValue) {
 		return equals(thatValue);
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/MapValue.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/MapValue.java
index 50618c4..dc5a5be 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/MapValue.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/MapValue.java
@@ -129,11 +129,6 @@
 
 	/**
 	 * @generated NOT
-	 */
-	@NonNull BagValue getValues();
-
-	/**
-	 * @generated NOT
 	 * @since 1.12
 	 */
 	default @NonNull MapTypeId getMapTypeId() { return getTypeId(); }
@@ -147,6 +142,11 @@
 	/**
 	 * @generated NOT
 	 */
+	@NonNull BagValue getValues();
+
+	/**
+	 * @generated NOT
+	 */
 	@NonNull Boolean includes(@Nullable Object value);
 
 	/**
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/TupleValue.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/TupleValue.java
index d8a4fe8..c032aeb 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/TupleValue.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/TupleValue.java
@@ -40,7 +40,7 @@
      */
 	default @NonNull TupleTypeId getTupleTypeId() { return getTypeId(); }
 
-    /**
+	/**
      * Obtains the tuple's type.
      *
      * @return its type
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/Value.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/Value.java
index 121aa99..542ba2d 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/Value.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/Value.java
@@ -221,6 +221,18 @@
 
 	/**
 	 * @generated NOT
+	 * @since 1.12
+	 */
+	default boolean mayBeInvalid() { return true; }
+
+	/**
+	 * @generated NOT
+	 * @since 1.12
+	 */
+	default boolean mayBeNull() { return true; }
+
+	/**
+	 * @generated NOT
 	 */
 	void toString(@NonNull StringBuilder s, int sizeLimit);
 }
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/analysis/SymbolicValue.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/analysis/SymbolicValue.java
index a1e21d5..4253d6f 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/analysis/SymbolicValue.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/analysis/SymbolicValue.java
@@ -13,7 +13,7 @@
 import org.eclipse.jdt.annotation.NonNull;
 
 /**
- * SymbolicValue defines a symbolic evauation result
+ * SymbolicValue defines a symbolic evaluation result
  * .
  * @since 1.12
  */
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationVisitor.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationVisitor.java
index 1710fd9..6443904 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationVisitor.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationVisitor.java
@@ -96,6 +96,7 @@
 import org.eclipse.ocl.pivot.values.IterableValue;
 import org.eclipse.ocl.pivot.values.MapValue;
 import org.eclipse.ocl.pivot.values.NullValue;
+import org.eclipse.ocl.pivot.values.SymbolicValue;
 import org.eclipse.ocl.pivot.values.Unlimited;
 import org.eclipse.ocl.pivot.values.UnlimitedNaturalValue;
 
@@ -332,8 +333,8 @@
 	@Override
 	public Object visitIfExp(@NonNull IfExp ifExp) {
 		OCLExpression condition = ifExp.getOwnedCondition();
-		Object acceptedValue = condition.accept(undecoratedVisitor);
-		Object evaluatedCondition = ValueUtil.asBoolean(acceptedValue);
+		Object conditionValue = condition.accept(undecoratedVisitor);
+		Object evaluatedCondition = ValueUtil.asBoolean(conditionValue);
 		OCLExpression expression = null;
 		if (evaluatedCondition == ValueUtil.TRUE_VALUE) {
 			expression = ifExp.getOwnedThen();
@@ -700,7 +701,7 @@
 					LibraryBinaryOperation.LibraryBinaryOperationExtension implementation = (LibraryBinaryOperation.LibraryBinaryOperationExtension) environmentFactory.getMetamodelManager().getImplementation(actualOperation);
 					try {
 						Object result = implementation.evaluate(context, operationCallExp.getTypeId(), sourceValue, onlyArgument);
-						assert !(result instanceof NullValue);
+						assert !(result instanceof NullValue) || (result instanceof SymbolicValue);
 						return result;
 					}
 					catch (InvalidValueException e) {
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicEvaluationVisitor.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicEvaluationVisitor.java
new file mode 100644
index 0000000..1524b0d
--- /dev/null
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicEvaluationVisitor.java
@@ -0,0 +1,296 @@
+/*******************************************************************************
+ * Copyright (c) 2010, 2018 Willink Transformations and others.
+ * All rights reserved.   This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v2.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v20.html
+ *
+ * Contributors:
+ *   E.D.Willink - Initial API and implementation
+ *******************************************************************************/
+
+package org.eclipse.ocl.pivot.internal.evaluation;
+
+import java.util.HashMap;
+import java.util.Map;
+
+import org.eclipse.jdt.annotation.NonNull;
+import org.eclipse.jdt.annotation.Nullable;
+import org.eclipse.ocl.pivot.AssociationClassCallExp;
+import org.eclipse.ocl.pivot.BooleanLiteralExp;
+import org.eclipse.ocl.pivot.CollectionItem;
+import org.eclipse.ocl.pivot.CollectionLiteralExp;
+import org.eclipse.ocl.pivot.CollectionRange;
+import org.eclipse.ocl.pivot.Constraint;
+import org.eclipse.ocl.pivot.Element;
+import org.eclipse.ocl.pivot.EnumLiteralExp;
+import org.eclipse.ocl.pivot.ExpressionInOCL;
+import org.eclipse.ocl.pivot.IfExp;
+import org.eclipse.ocl.pivot.IntegerLiteralExp;
+import org.eclipse.ocl.pivot.InvalidLiteralExp;
+import org.eclipse.ocl.pivot.LetExp;
+import org.eclipse.ocl.pivot.MapLiteralExp;
+import org.eclipse.ocl.pivot.MapLiteralPart;
+import org.eclipse.ocl.pivot.MessageExp;
+import org.eclipse.ocl.pivot.NullLiteralExp;
+import org.eclipse.ocl.pivot.OperationCallExp;
+import org.eclipse.ocl.pivot.OppositePropertyCallExp;
+import org.eclipse.ocl.pivot.PropertyCallExp;
+import org.eclipse.ocl.pivot.RealLiteralExp;
+import org.eclipse.ocl.pivot.ShadowExp;
+import org.eclipse.ocl.pivot.StateExp;
+import org.eclipse.ocl.pivot.StringLiteralExp;
+import org.eclipse.ocl.pivot.TupleLiteralExp;
+import org.eclipse.ocl.pivot.TupleLiteralPart;
+import org.eclipse.ocl.pivot.TypeExp;
+import org.eclipse.ocl.pivot.UnlimitedNaturalLiteralExp;
+import org.eclipse.ocl.pivot.UnspecifiedValueExp;
+import org.eclipse.ocl.pivot.Variable;
+import org.eclipse.ocl.pivot.VariableExp;
+import org.eclipse.ocl.pivot.evaluation.EvaluationVisitor;
+import org.eclipse.ocl.pivot.evaluation.Executor;
+import org.eclipse.ocl.pivot.utilities.MetamodelManager;
+import org.eclipse.ocl.pivot.utilities.PivotUtil;
+import org.eclipse.ocl.pivot.values.InvalidValueException;
+import org.eclipse.ocl.pivot.values.Value;
+
+/**
+ * A decorator for evaluation visitors that is installed when evaluation tracing
+ * is enabled, to trace interim evaluation results to the console.
+ * @since 1.12
+ */
+public class SymbolicEvaluationVisitor extends EvaluationVisitorDecorator implements EvaluationVisitor.EvaluationVisitorExtension {
+
+	private @NonNull Map<@NonNull Element, @Nullable Object> element2value = new HashMap<>();
+
+	/**
+	 * Initializes me with the visitor whose evaluation I trace to the console.
+	 *
+	 * @param decorated a real evaluation visitor
+	 */
+	public SymbolicEvaluationVisitor(@NonNull EvaluationVisitor decorated) {
+		super(decorated);
+	}
+
+	public void evaluate(@NonNull ExpressionInOCL expressionInOCL) {
+		Object result;
+		try {
+			result = evaluate(PivotUtil.getOwnedBody(expressionInOCL));
+		}
+		catch (InvalidValueException e) {
+			result = e;
+		}
+		element2value.put(expressionInOCL, result);
+	}
+
+	public @Nullable Object get(@NonNull Element element) {
+		Object object = element2value.get(element);
+		if (object == null) {
+			assert element2value.containsKey(element);
+		}
+		return object;
+	}
+
+	public boolean isDead(@NonNull Element element) {
+		return !element2value.containsKey(element);
+	}
+
+	public boolean mayBeInvalid(@NonNull Element element) {
+		Object object = element2value.get(element);
+		if (object == null) {
+			return true;
+		}
+		if (object instanceof Value) {
+			return ((Value)object).mayBeInvalid();
+		}
+		return false;
+	}
+
+	public boolean mayBeNull(@NonNull Element element) {
+		Object object = element2value.get(element);
+		if (object == null) {
+			return true;
+		}
+		if (object instanceof Value) {
+			return ((Value)object).mayBeNull();
+		}
+		return false;
+	}
+
+	/** @deprecated moved to Executor
+	 * @since 1.1*/
+	@Override
+	@Deprecated
+	public @NonNull Executor getExecutor() {
+		return ((EvaluationVisitor.EvaluationVisitorExtension)delegate).getExecutor();
+	}
+
+	/** @deprecated moved to Executor */
+	@Override
+	@Deprecated
+	public @NonNull MetamodelManager getMetamodelManager() {
+		return delegate.getMetamodelManager();
+	}
+
+	protected @Nullable Object trace(@NonNull Element expression, @Nullable Object value) {
+		if (value != null) {
+			Object old = element2value.put(expression, value);
+			assert old == null;
+		}
+		else {
+			assert !element2value.containsKey(expression);
+			element2value.put(expression, value);
+		}
+		return value;
+	}
+
+	@Override
+	public @Nullable Object visitAssociationClassCallExp(@NonNull AssociationClassCallExp callExp) {
+		return trace(callExp, delegate.visitAssociationClassCallExp(callExp));
+	}
+
+	@Override
+	public @Nullable Object visitBooleanLiteralExp(@NonNull BooleanLiteralExp literalExp) {
+		return trace(literalExp, delegate.visitBooleanLiteralExp(literalExp));
+	}
+
+	@Override
+	public @Nullable Object visitCollectionItem(@NonNull CollectionItem item) {
+		return trace(item, delegate.visitCollectionItem(item));
+	}
+
+	@Override
+	public @Nullable Object visitCollectionLiteralExp(@NonNull CollectionLiteralExp literalExp) {
+		return trace(literalExp, delegate.visitCollectionLiteralExp(literalExp));
+	}
+
+	@Override
+	public @Nullable Object visitCollectionRange(@NonNull CollectionRange range) {
+		return trace(range, delegate.visitCollectionRange(range));
+	}
+
+	@Override
+	public @Nullable Object visitConstraint(@NonNull Constraint constraint) {
+		return trace(constraint, delegate.visitConstraint(constraint));
+	}
+
+	@Override
+	public @Nullable Object visitEnumLiteralExp(@NonNull EnumLiteralExp literalExp) {
+		return trace(literalExp, delegate.visitEnumLiteralExp(literalExp));
+	}
+
+	@Override
+	public @Nullable Object visitExpressionInOCL(@NonNull ExpressionInOCL expression) {
+		return trace(expression, delegate.visitExpressionInOCL(expression));
+	}
+
+	@Override
+	public @Nullable Object visitIfExp(@NonNull IfExp ifExp) {
+		return trace(ifExp, delegate.visitIfExp(ifExp));
+	}
+
+	@Override
+	public @Nullable Object visitIntegerLiteralExp(@NonNull IntegerLiteralExp literalExp) {
+		return trace(literalExp, delegate.visitIntegerLiteralExp(literalExp));
+	}
+
+	@Override
+	public @Nullable Object visitInvalidLiteralExp(@NonNull InvalidLiteralExp literalExp) {
+		return trace(literalExp, delegate.visitInvalidLiteralExp(literalExp));
+	}
+
+	@Override
+	public @Nullable Object visitLetExp(@NonNull LetExp letExp) {
+		return trace(letExp, delegate.visitLetExp(letExp));
+	}
+
+	@Override
+	public @Nullable Object visitMapLiteralExp(@NonNull MapLiteralExp literalExp) {
+		return trace(literalExp, delegate.visitMapLiteralExp(literalExp));
+	}
+
+	@Override
+	public @Nullable Object visitMapLiteralPart(@NonNull MapLiteralPart range) {
+		return trace(range, delegate.visitMapLiteralPart(range));
+	}
+
+	@Override
+	public @Nullable Object visitMessageExp(@NonNull MessageExp messageExp) {
+		return trace(messageExp, delegate.visitMessageExp(messageExp));
+	}
+
+	@Override
+	public @Nullable Object visitNullLiteralExp(@NonNull NullLiteralExp literalExp) {
+		return trace(literalExp, delegate.visitNullLiteralExp(literalExp));
+	}
+
+	@Override
+	public @Nullable Object visitOperationCallExp(@NonNull OperationCallExp callExp) {
+		return trace(callExp, delegate.visitOperationCallExp(callExp));
+	}
+
+	@Override
+	public @Nullable Object visitOppositePropertyCallExp(@NonNull OppositePropertyCallExp callExp) {
+		return trace(callExp, delegate.visitOppositePropertyCallExp(callExp));
+	}
+
+	@Override
+	public @Nullable Object visitPropertyCallExp(@NonNull PropertyCallExp callExp) {
+		return trace(callExp, delegate.visitPropertyCallExp(callExp));
+	}
+
+	@Override
+	public @Nullable Object visitRealLiteralExp(@NonNull RealLiteralExp literalExp) {
+		return trace(literalExp, delegate.visitRealLiteralExp(literalExp));
+	}
+
+	@Override
+	public @Nullable Object visitShadowExp(@NonNull ShadowExp shadowExp) {
+		return trace(shadowExp, delegate.visitShadowExp(shadowExp));
+	}
+
+	@Override
+	public @Nullable Object visitStateExp(@NonNull StateExp stateExp) {
+		return trace(stateExp, delegate.visitStateExp(stateExp));
+	}
+
+	@Override
+	public @Nullable Object visitStringLiteralExp(@NonNull StringLiteralExp literalExp) {
+		return trace(literalExp, delegate.visitStringLiteralExp(literalExp));
+	}
+
+	@Override
+	public @Nullable Object visitTupleLiteralExp(@NonNull TupleLiteralExp literalExp) {
+		return trace(literalExp, delegate.visitTupleLiteralExp(literalExp));
+	}
+
+	@Override
+	public @Nullable Object visitTupleLiteralPart(@NonNull TupleLiteralPart part) {
+		return trace(part, delegate.visitTupleLiteralPart(part));
+	}
+
+	@Override
+	public @Nullable Object visitTypeExp(@NonNull TypeExp typeExp) {
+		return trace(typeExp, delegate.visitTypeExp(typeExp));
+	}
+
+	@Override
+	public @Nullable Object visitUnlimitedNaturalLiteralExp(@NonNull UnlimitedNaturalLiteralExp literalExp) {
+		return trace(literalExp, delegate.visitUnlimitedNaturalLiteralExp(literalExp));
+	}
+
+	@Override
+	public @Nullable Object visitUnspecifiedValueExp(@NonNull UnspecifiedValueExp unspecExp) {
+		return trace(unspecExp, delegate.visitUnspecifiedValueExp(unspecExp));
+	}
+
+	@Override
+	public @Nullable Object visitVariable(@NonNull Variable variable) {
+		return trace(variable, delegate.visitVariable(variable));
+	}
+
+	@Override
+	public @Nullable Object visitVariableExp(@NonNull VariableExp variableExp) {
+		return trace(variableExp, delegate.visitVariableExp(variableExp));
+	}
+}
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/MetamodelManagerInternal.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/MetamodelManagerInternal.java
index 8e9b3fd..4d90b24 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/MetamodelManagerInternal.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/MetamodelManagerInternal.java
@@ -19,6 +19,7 @@
 import org.eclipse.ocl.pivot.CompletePackage;
 import org.eclipse.ocl.pivot.Constraint;
 import org.eclipse.ocl.pivot.Element;
+import org.eclipse.ocl.pivot.ExpressionInOCL;
 import org.eclipse.ocl.pivot.Model;
 import org.eclipse.ocl.pivot.Namespace;
 import org.eclipse.ocl.pivot.OCLExpression;
@@ -27,6 +28,7 @@
 import org.eclipse.ocl.pivot.internal.complete.CompleteClassInternal;
 import org.eclipse.ocl.pivot.internal.complete.CompleteModelInternal;
 import org.eclipse.ocl.pivot.internal.complete.StandardLibraryInternal;
+import org.eclipse.ocl.pivot.internal.evaluation.SymbolicEvaluationVisitor;
 import org.eclipse.ocl.pivot.internal.utilities.EnvironmentFactoryInternal;
 import org.eclipse.ocl.pivot.internal.utilities.External2AS;
 import org.eclipse.ocl.pivot.library.LibraryProperty;
@@ -54,6 +56,12 @@
 	{
 		@NonNull FinalAnalysis getFinalAnalysis();
 		@NonNull FlowAnalysis getFlowAnalysis(@NonNull OCLExpression oclExpression);
+		/**
+		 * @since 1.12
+		 */
+		default @NonNull SymbolicEvaluationVisitor getSymbolicAnalysis(@NonNull ExpressionInOCL expressionInOCL, @Nullable Object context, @NonNull Object... parameters) {
+			throw new UnsupportedOperationException();
+		}
 		void resetFinalAnalysis();
 		void resetFlowAnalysis();
 	}
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/PivotMetamodelManager.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/PivotMetamodelManager.java
index 5858dc4..8895fa3 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/PivotMetamodelManager.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/PivotMetamodelManager.java
@@ -64,6 +64,7 @@
 import org.eclipse.ocl.pivot.MapType;
 import org.eclipse.ocl.pivot.Model;
 import org.eclipse.ocl.pivot.Namespace;
+import org.eclipse.ocl.pivot.NavigationCallExp;
 import org.eclipse.ocl.pivot.NullLiteralExp;
 import org.eclipse.ocl.pivot.OCLExpression;
 import org.eclipse.ocl.pivot.Operation;
@@ -83,8 +84,13 @@
 import org.eclipse.ocl.pivot.TupleType;
 import org.eclipse.ocl.pivot.Type;
 import org.eclipse.ocl.pivot.UnlimitedNaturalLiteralExp;
+import org.eclipse.ocl.pivot.Variable;
 import org.eclipse.ocl.pivot.VoidType;
 import org.eclipse.ocl.pivot.WildcardType;
+import org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment;
+import org.eclipse.ocl.pivot.evaluation.EvaluationVisitor;
+import org.eclipse.ocl.pivot.evaluation.ModelManager;
+import org.eclipse.ocl.pivot.ids.IdResolver;
 import org.eclipse.ocl.pivot.ids.TypeId;
 import org.eclipse.ocl.pivot.internal.PackageImpl;
 import org.eclipse.ocl.pivot.internal.compatibility.EMF_2_9;
@@ -96,6 +102,9 @@
 import org.eclipse.ocl.pivot.internal.complete.StandardLibraryInternal;
 import org.eclipse.ocl.pivot.internal.ecore.as2es.AS2Ecore;
 import org.eclipse.ocl.pivot.internal.ecore.es2as.Ecore2AS;
+import org.eclipse.ocl.pivot.internal.evaluation.BasicOCLExecutor;
+import org.eclipse.ocl.pivot.internal.evaluation.ExecutorInternal;
+import org.eclipse.ocl.pivot.internal.evaluation.SymbolicEvaluationVisitor;
 import org.eclipse.ocl.pivot.internal.library.ConstrainedOperation;
 import org.eclipse.ocl.pivot.internal.library.EInvokeOperation;
 import org.eclipse.ocl.pivot.internal.library.ImplementationManager;
@@ -113,6 +122,7 @@
 import org.eclipse.ocl.pivot.internal.utilities.OppositePropertyDetails;
 import org.eclipse.ocl.pivot.internal.utilities.PivotConstantsInternal;
 import org.eclipse.ocl.pivot.internal.utilities.PivotUtilInternal;
+import org.eclipse.ocl.pivot.internal.values.SymbolicNavigationCallValueImpl;
 import org.eclipse.ocl.pivot.library.LibraryFeature;
 import org.eclipse.ocl.pivot.library.LibraryProperty;
 import org.eclipse.ocl.pivot.library.UnsupportedOperation;
@@ -132,6 +142,7 @@
 import org.eclipse.ocl.pivot.utilities.TypeUtil;
 import org.eclipse.ocl.pivot.utilities.ValueUtil;
 import org.eclipse.ocl.pivot.values.IntegerValue;
+import org.eclipse.ocl.pivot.values.InvalidValueException;
 import org.eclipse.ocl.pivot.values.NumberValue;
 import org.eclipse.ocl.pivot.values.TemplateParameterSubstitutions;
 import org.eclipse.ocl.pivot.values.UnlimitedNaturalValue;
@@ -1177,6 +1188,90 @@
 		return flowAnalysis;
 	}
 
+	/**
+	 * @since 1.3
+	 */
+	@Override
+	public @NonNull SymbolicEvaluationVisitor getSymbolicAnalysis(@NonNull ExpressionInOCL expressionInOCL, @Nullable Object context, @NonNull Object... parameters) {
+		OCLExpression oclExpression = PivotUtil.getOwnedBody(expressionInOCL);
+		OCLExpression contextExpression = FlowAnalysis.getControlExpression(oclExpression);
+	//	Map<@NonNull OCLExpression, @NonNull FlowAnalysis> oclExpression2flowAnalysis2 = oclExpression2flowAnalysis;
+	//	if (oclExpression2flowAnalysis2 == null) {
+	//		oclExpression2flowAnalysis2 = oclExpression2flowAnalysis = new HashMap<>();
+	//	}
+//		ModelManager modelManager = environmentFactory.createModelManager(oclExpression);
+	//	Object context = null;
+		ModelManager modelManager = null;
+	//	EvaluationVisitor evaluationVisitor = environmentFactory.createEvaluationVisitor(null, expressionInOCL, modelManager);
+
+
+	//	if (modelManager == null) {
+			// let the evaluation environment create one
+			modelManager = environmentFactory.createModelManager(context);
+	//	}
+		// can determine a more appropriate context from the context
+		// variable of the expression, to account for stereotype constraints
+		//		context = HelperUtil.getConstraintContext(rootEnvironment, context, expression);
+	//	ExecutorInternal executor = createExecutor(modelManager);
+		ExecutorInternal executor = new BasicOCLExecutor((EnvironmentFactoryInternalExtension) environmentFactory, modelManager)
+		{
+		/*	@Override
+			protected @NonNull EvaluationEnvironmentExtension createRootEvaluationEnvironment(@NonNull NamedElement executableObject) {
+			//	return super.createRootEvaluationEnvironment(executableObject);
+				return new BasicEvaluationEnvironment(this, executableObject)
+				{
+					@Override
+					public void add(@NonNull TypedElement referredVariable, @Nullable Object value) {
+						// TODO Auto-generated method stub
+						super.add(referredVariable, value);
+					}
+				};
+			} */
+
+			@Override
+			public @Nullable Object internalExecuteNavigationCallExp(@NonNull NavigationCallExp navigationCallExp, @NonNull Property referredProperty, @Nullable Object sourceValue) {
+				return new SymbolicNavigationCallValueImpl(navigationCallExp, sourceValue);
+			}
+
+			@Override
+			public Object internalExecuteOperationCallExp(@NonNull OperationCallExp operationCallExp, @Nullable Object @NonNull [] sourceAndArgumentValues) {
+				return super.internalExecuteOperationCallExp(operationCallExp, sourceAndArgumentValues);
+			}
+
+		};
+		EvaluationEnvironment evaluationEnvironment = executor.initializeEvaluationEnvironment(expressionInOCL);
+		IdResolver idResolver = environmentFactory.getIdResolver();
+		Variable contextVariable = expressionInOCL.getOwnedContext();
+		if (contextVariable != null) {
+			Object value = context; //new SymbolicVariableValueImpl(contextVariable); //idResolver.boxedValueOf(context);
+			evaluationEnvironment.add(contextVariable, idResolver.boxedValueOf(value));
+		}
+		int i = 0;
+		for (Variable parameterVariable : PivotUtil.getOwnedParameters(expressionInOCL)) {
+			evaluationEnvironment.add(parameterVariable, idResolver.boxedValueOf(parameters[i++]));
+		}
+		EvaluationVisitor evaluationVisitor =  executor.getEvaluationVisitor();
+
+
+
+
+//		ExecutorInternal executor = ((EnvironmentFactoryExtension)environmentFactory).createExecutor(modelManager);
+//		EvaluationVisitor evaluationVisitor = executor.getEvaluationVisitor();
+		SymbolicEvaluationVisitor symbolicEvaluationVisitor = new SymbolicEvaluationVisitor(evaluationVisitor);
+		try {
+			symbolicEvaluationVisitor.evaluate(expressionInOCL);
+		}
+		catch (InvalidValueException e) {
+			// Ok so some results are unarguably invalid.
+		}
+	//	FlowAnalysis flowAnalysis = oclExpression2flowAnalysis2.get(contextExpression);
+	//	if (flowAnalysis == null) {
+	//		flowAnalysis = environmentFactory.createFlowAnalysis(contextExpression);
+	//		oclExpression2flowAnalysis2.put(contextExpression, flowAnalysis);
+	//	}
+		return symbolicEvaluationVisitor;
+	}
+
 	@Override
 	public @Nullable GenPackage getGenPackage(@NonNull String nsURI) {
 		if (genPackageMap != null) {
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyEqualOperation.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyEqualOperation.java
index 848095f..1f018af 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyEqualOperation.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyEqualOperation.java
@@ -39,7 +39,7 @@
 		if (left == null) {
 			return right == null;
 		}
-		else if ((left instanceof Type) && (right instanceof Type)){
+		else if ((left instanceof Type) && (right instanceof Type)) {
 			boolean result = ((Type) left).getTypeId().equals(((Type) right).getTypeId());		// FIXME is this a sound/efficient tradeoff for not boxing?
 			return result;
 		}
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyToStringOperation.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyToStringOperation.java
index 73deadd..d83a925 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyToStringOperation.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyToStringOperation.java
@@ -12,8 +12,10 @@
 
 import org.eclipse.jdt.annotation.NonNull;
 import org.eclipse.jdt.annotation.Nullable;
+import org.eclipse.ocl.pivot.internal.values.SymbolicStringValueImpl;
 import org.eclipse.ocl.pivot.library.AbstractSimpleUnaryOperation;
 import org.eclipse.ocl.pivot.values.InvalidValueException;
+import org.eclipse.ocl.pivot.values.SymbolicValue;
 
 /**
  * OclAnyToStringOperation realises the OclAny::toString() library operation.
@@ -21,6 +23,11 @@
 public class OclAnyToStringOperation extends AbstractSimpleUnaryOperation
 {
 	public static final @NonNull OclAnyToStringOperation INSTANCE = new OclAnyToStringOperation();
+	/**
+	 * @since 1.12
+	 */
+	public static final OclAnyToStringOperation.@NonNull Symbolic INSTANCE2 = new OclAnyToStringOperation.Symbolic();
+
 
 	@Override
 	public @NonNull String evaluate(@Nullable Object sourceVal) {
@@ -29,4 +36,18 @@
 		}
 		return sourceVal != null ? oclToString(sourceVal) : NULL_STRING;
 	}
+
+	private static class Symbolic extends AbstractSimpleUnaryOperation
+	{
+		@Override
+		public @NonNull Object evaluate(@Nullable Object sourceVal) {
+			if (sourceVal instanceof InvalidValueException)	{				// FIXME Remove this once CG has proper invalid analysis
+				throw (InvalidValueException)sourceVal;
+			}
+			if (sourceVal instanceof SymbolicValue)	{				// FIXME Remove this once CG has proper invalid analysis
+				return new SymbolicStringValueImpl(sourceVal);
+			}
+			return sourceVal != null ? oclToString(sourceVal) : NULL_STRING;
+		}
+	}
 }
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/AbstractEnvironmentFactory.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/AbstractEnvironmentFactory.java
index c473492..29cfd5a 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/AbstractEnvironmentFactory.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/AbstractEnvironmentFactory.java
@@ -38,6 +38,7 @@
 import org.eclipse.ocl.pivot.LanguageExpression;
 import org.eclipse.ocl.pivot.LoopExp;
 import org.eclipse.ocl.pivot.NamedElement;
+import org.eclipse.ocl.pivot.NavigationCallExp;
 import org.eclipse.ocl.pivot.OCLExpression;
 import org.eclipse.ocl.pivot.Operation;
 import org.eclipse.ocl.pivot.OperationCallExp;
@@ -304,7 +305,20 @@
 		// can determine a more appropriate context from the context
 		// variable of the expression, to account for stereotype constraints
 		//		context = HelperUtil.getConstraintContext(rootEnvironment, context, expression);
-		ExecutorInternal executor = createExecutor(modelManager);
+	//	ExecutorInternal executor = createExecutor(modelManager);
+		ExecutorInternal executor = new BasicOCLExecutor(this, modelManager)
+		{
+			@Override
+			public @Nullable Object internalExecuteNavigationCallExp(@NonNull NavigationCallExp navigationCallExp, @NonNull Property referredProperty, @Nullable Object sourceValue) {
+				return super.internalExecuteNavigationCallExp(navigationCallExp, referredProperty, sourceValue);
+			}
+
+			@Override
+			public Object internalExecuteOperationCallExp(@NonNull OperationCallExp operationCallExp, @Nullable Object @NonNull [] sourceAndArgumentValues) {
+				return super.internalExecuteOperationCallExp(operationCallExp, sourceAndArgumentValues);
+			}
+
+		};
 		EvaluationEnvironment evaluationEnvironment = executor.initializeEvaluationEnvironment(expression);
 		Variable contextVariable = expression.getOwnedContext();
 		if (contextVariable != null) {
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/PivotUtil.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/PivotUtil.java
index 33a2867..e4ccf12 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/PivotUtil.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/PivotUtil.java
@@ -1521,6 +1521,13 @@
 	}
 
 	/**
+	 * @since 1.12
+	 */
+	public static @NonNull Iterable<@NonNull Variable> getOwnedParameters(@NonNull ExpressionInOCL expressionInOCL) {
+		return ClassUtil.nullFree(expressionInOCL.getOwnedParameters());
+	}
+
+	/**
 	 * @since 1.3
 	 */
 	public static @NonNull Iterable<@NonNull Parameter> getOwnedParameters(@NonNull Operation operation) {
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/ValueUtil.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/ValueUtil.java
index c9031ed..3644087 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/ValueUtil.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/ValueUtil.java
@@ -89,6 +89,7 @@
 import org.eclipse.ocl.pivot.values.RealValue;
 import org.eclipse.ocl.pivot.values.SequenceValue;
 import org.eclipse.ocl.pivot.values.SetValue;
+import org.eclipse.ocl.pivot.values.SymbolicValue;
 import org.eclipse.ocl.pivot.values.TupleValue;
 import org.eclipse.ocl.pivot.values.UniqueCollectionValue;
 import org.eclipse.ocl.pivot.values.Unlimited;
@@ -886,6 +887,9 @@
 	}
 
 	public static boolean isBoxed(@Nullable Object object) {
+		if (object instanceof SymbolicValue) {
+			return true;
+		}
 		if (object instanceof NullValue) {
 			return false;
 		}
diff --git a/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/test/xtext/FlowAnalysisTests.java b/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/test/xtext/FlowAnalysisTests.java
index ad2fef3..c453f21 100644
--- a/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/test/xtext/FlowAnalysisTests.java
+++ b/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/test/xtext/FlowAnalysisTests.java
@@ -15,21 +15,28 @@
 import org.eclipse.emf.common.util.URI;
 import org.eclipse.emf.ecore.resource.Resource;
 import org.eclipse.jdt.annotation.NonNull;
+import org.eclipse.jdt.annotation.Nullable;
 import org.eclipse.ocl.examples.pivot.tests.TestOCL;
 import org.eclipse.ocl.examples.xtext.tests.XtextTestCase;
 import org.eclipse.ocl.pivot.Constraint;
+import org.eclipse.ocl.pivot.ExpressionInOCL;
 import org.eclipse.ocl.pivot.IfExp;
 import org.eclipse.ocl.pivot.IteratorExp;
 import org.eclipse.ocl.pivot.LetExp;
 import org.eclipse.ocl.pivot.Model;
 import org.eclipse.ocl.pivot.NullLiteralExp;
 import org.eclipse.ocl.pivot.OCLExpression;
+import org.eclipse.ocl.pivot.Operation;
 import org.eclipse.ocl.pivot.OperationCallExp;
 import org.eclipse.ocl.pivot.PropertyCallExp;
+import org.eclipse.ocl.pivot.StringLiteralExp;
 import org.eclipse.ocl.pivot.VariableExp;
+import org.eclipse.ocl.pivot.ids.TypeId;
+import org.eclipse.ocl.pivot.internal.evaluation.SymbolicEvaluationVisitor;
 import org.eclipse.ocl.pivot.internal.manager.FlowAnalysis;
 import org.eclipse.ocl.pivot.internal.manager.MetamodelManagerInternal;
 import org.eclipse.ocl.pivot.internal.utilities.EnvironmentFactoryInternal.EnvironmentFactoryInternalExtension;
+import org.eclipse.ocl.pivot.internal.values.SymbolicUnknownValueImpl;
 import org.eclipse.ocl.pivot.resource.ASResource;
 import org.eclipse.ocl.pivot.utilities.NameUtil;
 import org.eclipse.ocl.pivot.utilities.OCL;
@@ -77,7 +84,7 @@
 				flowAnalysis.isNonNull(asExpression));
 		}
 
-		protected @NonNull OCLExpression createTestModel(@NonNull String invariantName, @NonNull String invariantBody) throws IOException, ParserException {
+		protected @NonNull ExpressionInOCL createInvariantTestModel(@NonNull String invariantName, @NonNull String invariantBody) throws IOException, ParserException {
 			String testContext =
 					"package deductions : ded = 'http://deductions'\n" +
 							"{\n" +
@@ -100,7 +107,37 @@
 			org.eclipse.ocl.pivot.Package deductionsPackage = NameUtil.getNameable(model.getOwnedPackages(), "deductions");
 			org.eclipse.ocl.pivot.Class deductionsClass = NameUtil.getNameable(deductionsPackage.getOwnedClasses(), "Deductions");
 			Constraint asInvariant = NameUtil.getNameable(deductionsClass.getOwnedInvariants(), invariantName);
-			return ((EnvironmentFactoryInternalExtension)environmentFactory).parseSpecification(asInvariant.getOwnedSpecification()).getOwnedBody();
+			return ((EnvironmentFactoryInternalExtension)environmentFactory).parseSpecification(asInvariant.getOwnedSpecification());
+		}
+
+		protected @NonNull ExpressionInOCL createQueryTestModel(@NonNull String queryName, @NonNull String querySignature, @NonNull String queryBody) throws IOException, ParserException {
+			String testContext =
+					"package deductions : ded = 'http://deductions'\n" +
+							"{\n" +
+							"  class Deductions\n" +
+							"  {\n" +
+							"    property dummy : Dummy[?];\n" +
+							"    property x : Integer[?];\n" +
+							"    operation " + querySignature + " {\nbody: " + queryBody + ";\n}\n" +
+							"  }\n" +
+							"  class Dummy\n" +
+							"  {\n" +
+							"    property dummy : Dummy[?];\n" +
+							"    operation func(i : Integer, j : Integer) : Dummy[?];\n" +
+							"  }\n" +
+							"}";
+			String fileName = "FlowAnalysis_" + queryName;
+			createOCLinEcoreFile(fileName + ".oclinecore", testContext);
+			Resource asResource = doLoad_Concrete(fileName, "oclinecore");
+			Model model = PivotUtil.getModel(asResource);
+			org.eclipse.ocl.pivot.Package deductionsPackage = NameUtil.getNameable(model.getOwnedPackages(), "deductions");
+			org.eclipse.ocl.pivot.Class deductionsClass = NameUtil.getNameable(deductionsPackage.getOwnedClasses(), "Deductions");
+			Operation asOperation = NameUtil.getNameable(deductionsClass.getOwnedOperations(), queryName);
+			return ((EnvironmentFactoryInternalExtension)environmentFactory).parseSpecification(asOperation.getBodyExpression());
+		}
+
+		protected @NonNull OCLExpression createTestModel(@NonNull String invariantName, @NonNull String invariantBody) throws IOException, ParserException {
+			return createInvariantTestModel(invariantName, invariantBody).getOwnedBody();
 		}
 
 		public Resource doLoad_Concrete(@NonNull String stem, @NonNull String extension) throws IOException {
@@ -132,6 +169,11 @@
 			MetamodelManagerInternal metamodelManager = getMetamodelManager();
 			return ((MetamodelManagerInternal.MetamodelManagerInternalExtension2)metamodelManager).getFlowAnalysis(asExpression);
 		}
+
+		protected @NonNull SymbolicEvaluationVisitor getSymbolicAnalysis(@NonNull ExpressionInOCL asExpressionInOCL, @Nullable Object context, @NonNull Object... parameters) {
+			MetamodelManagerInternal metamodelManager = getMetamodelManager();
+			return ((MetamodelManagerInternal.MetamodelManagerInternalExtension2)metamodelManager).getSymbolicAnalysis(asExpressionInOCL, context, parameters);
+		}
 	}
 
 	public void testFlowAnalysis_SimpleProperty() throws Exception {
@@ -199,24 +241,91 @@
 		ocl.dispose();
 	}
 
-	/*	public void testFlowAnalysis_SimpleIfNameGuard() throws Exception {
+	public void testFlowAnalysis_SimpleIfNameGuard() throws Exception {
 		MyOCL ocl = new MyOCL();
-		LetExp asLetExp = (LetExp) ocl.createTestModel("SimpleIfNameGuard",
-				"let v : String[?] = x?.toString() in if v = null then 'null' else v endif");
+		ExpressionInOCL asExpressionInOCL = ocl.createInvariantTestModel("SimpleIfNameGuard",
+				"(let v : String[?] = self?.toString() in if v = null then 'null' else v endif) <> null");
+		OperationCallExp asOperationCallExp = (OperationCallExp) asExpressionInOCL.getOwnedBody();
+		LetExp asLetExp = (LetExp) PivotUtil.getOwnedSource(asOperationCallExp);
+//		LetExp asLetExp = (LetExp) PivotUtil.getOwnedInit(PivotUtil.getOwnedSource(asOperationCallExp));
 		OperationCallExp asLetVariableInit = (OperationCallExp) PivotUtil.getOwnedInit(PivotUtil.getOwnedVariable(asLetExp));
-		IfExp asIn = (IfExp) PivotUtil.getOwnedIn(asLetExp);
-		OperationCallExp asCondition = (OperationCallExp) PivotUtil.getOwnedCondition(asIn);
-		StringLiteralExp asThenLiteralExp = (StringLiteralExp) PivotUtil.getOwnedThen(asIn);
-		VariableExp asElseVariableExp = (VariableExp) PivotUtil.getOwnedElse(asIn);
+		IfExp asIf = (IfExp) PivotUtil.getOwnedIn(asLetExp);
+		OperationCallExp asCondition = (OperationCallExp) PivotUtil.getOwnedCondition(asIf);
+		StringLiteralExp asThenLiteralExp = (StringLiteralExp) PivotUtil.getOwnedThen(asIf);
+		VariableExp asElseVariableExp = (VariableExp) PivotUtil.getOwnedElse(asIf);
 		VariableExp asConditionVariableExp = (VariableExp) PivotUtil.getOwnedSource(asCondition);
 		//		ocl.assertIsNotKnown(asLetVariableInit);
 		//		ocl.assertIsNotKnown(asConditionVariableExp);
 		//		ocl.assertIsNonNull(asThenLiteralExp);
 		//		ocl.assertIsNotKnown(asElseVariableExp);
-		ocl.assertIsNonNull(asIn);
-		ocl.assertIsNonNull(asLetExp);
+
+		SymbolicEvaluationVisitor symbolicAnalysis1 = ocl.getSymbolicAnalysis(asExpressionInOCL, null);
+		assert !symbolicAnalysis1.mayBeNull(asExpressionInOCL);
+		assert !symbolicAnalysis1.mayBeNull(asIf);
+		assert !symbolicAnalysis1.mayBeNull(asLetExp);
+		assert ocl.getIdResolver().oclEquals(symbolicAnalysis1.get(asIf), "null");
+		assert symbolicAnalysis1.isDead(asElseVariableExp);
+
+		SymbolicEvaluationVisitor symbolicAnalysis2 = ocl.getSymbolicAnalysis(asExpressionInOCL, new SymbolicUnknownValueImpl(TypeId.STRING, false, false));
+		assert !symbolicAnalysis2.mayBeNull(asExpressionInOCL);
+		assert !symbolicAnalysis2.mayBeNull(asIf);
+		assert !symbolicAnalysis2.mayBeNull(asLetExp);
+//		assert ocl.getIdResolver().oclEquals(symbolicAnalysis2.get(asIf), "null");
+		assert symbolicAnalysis2.isDead(asThenLiteralExp);
 		ocl.dispose();
-	} */
+	}
+
+	public void testSymbolicAnalysis_BadDivide() throws Exception {
+		MyOCL ocl = new MyOCL();
+		ExpressionInOCL asExpressionInOCL = ocl.createQueryTestModel("BadDivide", "BadDivide(num : Real, den : Real) : Real",
+	//			"let num = 5.0 in den = 0.0 in num / den");
+				"num / den");
+		OperationCallExp asOperationCallExp = (OperationCallExp) asExpressionInOCL.getOwnedBody();
+		VariableExp asNumExp = (VariableExp) PivotUtil.getOwnedSource(asOperationCallExp);
+		VariableExp asDenExp = (VariableExp) PivotUtil.getOwnedArgument(asOperationCallExp, 0);
+
+		SymbolicEvaluationVisitor symbolicAnalysis1 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, 5.0, 0.0);
+		assert !symbolicAnalysis1.mayBeNull(asExpressionInOCL);
+		assert !symbolicAnalysis1.mayBeNull(asNumExp);
+		assert !symbolicAnalysis1.mayBeNull(asDenExp);
+		assert !symbolicAnalysis1.mayBeInvalid(asNumExp);
+		assert !symbolicAnalysis1.mayBeInvalid(asDenExp);
+		assert symbolicAnalysis1.mayBeInvalid(asOperationCallExp);
+
+		SymbolicEvaluationVisitor symbolicAnalysis2 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, 5.0, 1.0);
+		assert !symbolicAnalysis2.mayBeNull(asExpressionInOCL);
+		assert !symbolicAnalysis2.mayBeNull(asNumExp);
+		assert !symbolicAnalysis2.mayBeNull(asDenExp);
+		assert !symbolicAnalysis2.mayBeInvalid(asNumExp);
+		assert !symbolicAnalysis2.mayBeInvalid(asDenExp);
+		assert !symbolicAnalysis2.mayBeInvalid(asOperationCallExp);
+
+		SymbolicEvaluationVisitor symbolicAnalysis3 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, new SymbolicUnknownValueImpl(TypeId.REAL, false, false), 0.0);
+		assert !symbolicAnalysis3.mayBeNull(asExpressionInOCL);
+		assert !symbolicAnalysis3.mayBeNull(asNumExp);
+		assert !symbolicAnalysis3.mayBeNull(asDenExp);
+		assert !symbolicAnalysis3.mayBeInvalid(asNumExp);
+		assert !symbolicAnalysis3.mayBeInvalid(asDenExp);
+		assert symbolicAnalysis3.mayBeInvalid(asOperationCallExp);
+
+		SymbolicEvaluationVisitor symbolicAnalysis4 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, new SymbolicUnknownValueImpl(TypeId.REAL, false, false), 1.0);
+		assert !symbolicAnalysis4.mayBeNull(asExpressionInOCL);
+		assert !symbolicAnalysis4.mayBeNull(asNumExp);
+		assert !symbolicAnalysis4.mayBeNull(asDenExp);
+		assert !symbolicAnalysis4.mayBeInvalid(asNumExp);
+		assert !symbolicAnalysis4.mayBeInvalid(asDenExp);
+		assert !symbolicAnalysis4.mayBeInvalid(asOperationCallExp);
+//		assert ocl.getIdResolver().oclEquals(symbolicAnalysis1.get(asIf), "null");
+//		assert symbolicAnalysis1.isDead(asElseVariableExp);
+
+//		SymbolicEvaluationVisitor symbolicAnalysis2 = ocl.getSymbolicAnalysis(asExpressionInOCL, new SymbolicUnknownValueImpl(TypeId.STRING, false, false));
+//		assert !symbolicAnalysis2.mayBeNull(asExpressionInOCL);
+//		assert !symbolicAnalysis2.mayBeNull(asIf);
+//		assert !symbolicAnalysis2.mayBeNull(asLetExp);
+//		assert ocl.getIdResolver().oclEquals(symbolicAnalysis2.get(asIf), "null");
+//		assert symbolicAnalysis2.isDead(asThenLiteralExp); */
+		ocl.dispose();
+	}
 
 	public void testFlowAnalysis_ImpliesPropertyGuard() throws Exception {
 		MyOCL ocl = new MyOCL();