From 2cb56f643b01b9f6009c0e60fb7e0fa389266952 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 6 Jul 2017 15:57:34 +0100
Subject: [PATCH] Do not constant propagate multiplication unconditionally

The previous code was a non-trivial expression always returning true.

Fixes: #351
---
 src/goto-symex/goto_symex_state.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index d88e9c68bac..361669c5bec 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -125,8 +125,12 @@ bool goto_symex_statet::constant_propagation(const exprt &expr) const
   {
     // propagate stuff with sizeof in it
     forall_operands(it, expr)
+    {
       if(it->find(ID_C_c_sizeof_type).is_not_nil())
         return true;
+      else if(!constant_propagation(*it))
+        return false;
+    }
 
     return true;
   }