From 829068ffe7029177bbf6209949f9b53d6e55a522 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 21 Jun 2016 18:51:29 +0000 Subject: [PATCH] Don't require the simplifier to solve this regression test --- regression/cbmc/null3/test.desc | 1 - 1 file changed, 1 deletion(-) diff --git a/regression/cbmc/null3/test.desc b/regression/cbmc/null3/test.desc index 60ac44fc4e0..9efefbc7362 100644 --- a/regression/cbmc/null3/test.desc +++ b/regression/cbmc/null3/test.desc @@ -3,7 +3,6 @@ main.c ^EXIT=0$ ^SIGNAL=0$ -^Generated .* VCC\(s\), 0 remaining after simplification$ ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring