From 57b94c4edd3767d8615d0ac2c3fb3bdb0dcb373c Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 25 Feb 2016 21:19:20 +0000
Subject: [PATCH] Force the guard to false_exprt() whenever false is added to
 the conjunction

Since r6259 guardt::is_false() is just exprt's is_false() instead of
a full loop testing each conjunct.
---
 regression/cbmc/guard1/main.c    | 22 ++++++++++++++++++++++
 regression/cbmc/guard1/test.desc |  7 +++++++
 src/util/guard.cpp               |  2 +-
 3 files changed, 30 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/guard1/main.c
 create mode 100644 regression/cbmc/guard1/test.desc

diff --git a/regression/cbmc/guard1/main.c b/regression/cbmc/guard1/main.c
new file mode 100644
index 00000000000..d84f80cd009
--- /dev/null
+++ b/regression/cbmc/guard1/main.c
@@ -0,0 +1,22 @@
+int main()
+{
+int i;
+int j;
+while(i) j = j + 1;
+}
+
+/*
+#include <assert.h>
+
+int main (void) {
+	int i;
+
+	while (1) {
+		i++;
+	}
+
+	assert(0);
+
+	return;
+}
+*/
diff --git a/regression/cbmc/guard1/test.desc b/regression/cbmc/guard1/test.desc
new file mode 100644
index 00000000000..a6acc8553dc
--- /dev/null
+++ b/regression/cbmc/guard1/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--depth 19
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/src/util/guard.cpp b/src/util/guard.cpp
index 05deab612d0..add5a4dd127 100644
--- a/src/util/guard.cpp
+++ b/src/util/guard.cpp
@@ -99,7 +99,7 @@ void guardt::add(const exprt &expr)
 
   if(is_false() || expr.is_true())
     return;
-  else if(is_true())
+  else if(is_true() || expr.is_false())
   {
     *this=expr;