From 37440ac27c172d219d669a8ed45fe834bb85a3f3 Mon Sep 17 00:00:00 2001
From: Saswat Padhi <saspadhi@amazon.com>
Date: Fri, 19 Feb 2021 11:33:48 -0500
Subject: [PATCH] Fixed weakest precondition for code_assertt

The existing wp function treated an assert statement the same way as a skip statement. This commit fixes this behavior as per standard Hoare logic rules.
---
 src/goto-programs/wp.cpp | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp
index c8ce71ae28b..3f22bd5433d 100644
--- a/src/goto-programs/wp.cpp
+++ b/src/goto-programs/wp.cpp
@@ -213,6 +213,14 @@ exprt wp_assign(
   return pre;
 }
 
+exprt wp_assert(
+  const code_assertt &code,
+  const exprt &post,
+  const namespacet &)
+{
+  return and_exprt(code.assertion(), post);
+}
+
 exprt wp_assume(
   const code_assumet &code,
   const exprt &post,
@@ -250,7 +258,7 @@ exprt wp(
   else if(statement==ID_decl)
     return wp_decl(to_code_decl(code), post, ns);
   else if(statement==ID_assert)
-    return post;
+    return wp_assert(to_code_assert(code), post, ns);
   else if(statement==ID_expression)
     return post;
   else if(statement==ID_printf)