diff --git a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
index ea0c64729ffd2349a13a458191e2afbdb84fa5fc..14279414e5d83e23965d98af9f5141d5e4385a62 100644
--- a/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
+++ b/src/main/java/de/tla2b/analysis/PredicateVsExpression.java
@@ -50,7 +50,8 @@ public class PredicateVsExpression extends BuiltInOPs implements BBuildIns {
 				case OPCODE_lor: // \/
 				case OPCODE_equiv: // \equiv
 				case OPCODE_implies: // =>
-				case OPCODE_lnot: // \lnot
+				case OPCODE_neg: // \neg
+				case OPCODE_lnot: // ~ / \lnot
 				case OPCODE_be: // \E x \in S : P
 				case OPCODE_bf: // \A x \in S : P
 				case OPCODE_in: // \in
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 906ef124cd25d261b46651f0a9ab88f4e40c50ab..5681a7ecfe8ad801aa2ace4508e3b712c1addef3 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -996,7 +996,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
 						.map(this::visitExprOrOpArgNodePredicate).collect(Collectors.toList()));
 				break;
 
-			case OPCODE_lnot: // \lnot
+			case OPCODE_neg: // \neg
+			case OPCODE_lnot: // ~ / \lnot
 				returnNode = new ANegationPredicate(visitExprOrOpArgNodePredicate(n.getArgs()[0]));
 				break;
 
@@ -1144,7 +1145,8 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
 			case OPCODE_cl: // $ConjList
 			case OPCODE_dl: // $DisjList
 			case OPCODE_lor: // \/
-			case OPCODE_lnot: // \lnot
+			case OPCODE_neg: // \neg
+			case OPCODE_lnot: // ~ / \lnot
 			case OPCODE_in: // \in
 			case OPCODE_notin: // \notin
 			case OPCODE_eq: // =
diff --git a/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java b/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
index 5af94a9eb50ccca51eb68e77507254ba4af81566..611cecbaa69e56a2601d77167fc63ca2f4a45b8c 100644
--- a/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
+++ b/src/test/java/de/tla2b/typechecking/LogicOperatorsTest.java
@@ -58,6 +58,18 @@ public class LogicOperatorsTest {
 		assertEquals("BOOL", t.getConstantType("k3"));
 	}
 
+	@Test
+	public void testNeg() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+				+ "CONSTANTS k, k2\n"
+				+ "ASSUME k = \\neg k2 \n"
+				+ "=================================";
+
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("BOOL", t.getConstantType("k"));
+		assertEquals("BOOL", t.getConstantType("k2"));
+	}
+
 	@Test(expected = TypeErrorException.class)
 	public void testLogicOperatorsError() throws TLA2BException {
 		final String module = "-------------- MODULE Testing ----------------\n"