From 08d43f9271f9ff6ff09b8ae0883f01f1f38a7fe5 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 6 Aug 2019 16:53:49 +0100 Subject: [PATCH] Activate regression tests previously KNOWNBUG These tests can now be executed in our test suite. --- regression/cbmc-concurrency/norace_array1/test.desc | 2 +- regression/cbmc-concurrency/norace_array2/test.desc | 2 +- regression/cbmc-concurrency/struct_and_array1/test.desc | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/regression/cbmc-concurrency/norace_array1/test.desc b/regression/cbmc-concurrency/norace_array1/test.desc index c239dca4b3..8ecf05b6d5 100644 --- a/regression/cbmc-concurrency/norace_array1/test.desc +++ b/regression/cbmc-concurrency/norace_array1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG pthread +CORE pthread main.c ^EXIT=0$ diff --git a/regression/cbmc-concurrency/norace_array2/test.desc b/regression/cbmc-concurrency/norace_array2/test.desc index c239dca4b3..8ecf05b6d5 100644 --- a/regression/cbmc-concurrency/norace_array2/test.desc +++ b/regression/cbmc-concurrency/norace_array2/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG pthread +CORE pthread main.c ^EXIT=0$ diff --git a/regression/cbmc-concurrency/struct_and_array1/test.desc b/regression/cbmc-concurrency/struct_and_array1/test.desc index 52168c7eba..8ecf05b6d5 100644 --- a/regression/cbmc-concurrency/struct_and_array1/test.desc +++ b/regression/cbmc-concurrency/struct_and_array1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE pthread main.c ^EXIT=0$