diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp
index 9286a3ecc..5cab13d8d 100644
--- a/src/temporal-logic/normalize_property.cpp
+++ b/src/temporal-logic/normalize_property.cpp
@@ -53,6 +53,16 @@ exprt normalize_pre_not(not_exprt expr)
     // ¬Xφ --> X¬φ
     return X_exprt{not_exprt{to_X_expr(op).op()}};
   }
+  else if(op.id() == ID_sva_always)
+  {
+    // ¬ sva_always φ --> sva_s_eventually ¬φ
+    return sva_s_eventually_exprt{not_exprt{to_sva_always_expr(op).op()}};
+  }
+  else if(op.id() == ID_sva_s_eventually)
+  {
+    // ¬ sva_s_eventually φ --> sva_always ¬φ
+    return sva_always_exprt{not_exprt{to_sva_eventually_expr(op).op()}};
+  }
 
   return std::move(expr);
 }
diff --git a/src/temporal-logic/normalize_property.h b/src/temporal-logic/normalize_property.h
index 8c7a75e71..31bf4af45 100644
--- a/src/temporal-logic/normalize_property.h
+++ b/src/temporal-logic/normalize_property.h
@@ -31,6 +31,8 @@ Author: Daniel Kroening, dkr@amazon.com
 /// a sva_reject_on b --> ¬a ∧ b
 /// a sva_sync_accept_on b --> a ∨ b
 /// a sva_sync_reject_on b --> ¬a ∧ b
+/// ¬ sva_s_eventually φ --> sva_always ¬φ
+/// ¬ sva_always φ --> sva_s_eventually ¬φ
 /// ¬Xφ --> X¬φ
 /// ¬¬φ --> φ
 /// ¬Gφ --> F¬φ