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 + +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;