From 7486222e8c44ebba60764f021642b33d9f6fb983 Mon Sep 17 00:00:00 2001
From: martin <martin@michael>
Date: Tue, 15 Jun 2021 17:30:01 +0100
Subject: [PATCH] Add the smt-backend tags to tests that use --z3

This means that the core tests will run cleanly without z3 on the path.
---
 regression/cbmc/struct15/test.desc | 2 +-
 regression/cbmc/z3/invalid.desc    | 2 +-
 regression/cbmc/z3/valid.desc      | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/regression/cbmc/struct15/test.desc b/regression/cbmc/struct15/test.desc
index 3faa87ff9fa..81a142d267f 100644
--- a/regression/cbmc/struct15/test.desc
+++ b/regression/cbmc/struct15/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE smt-backend
 main.c
 --trace --z3
 ^EXIT=0$
diff --git a/regression/cbmc/z3/invalid.desc b/regression/cbmc/z3/invalid.desc
index e6bc587e7ad..a2f83971f8f 100644
--- a/regression/cbmc/z3/invalid.desc
+++ b/regression/cbmc/z3/invalid.desc
@@ -1,4 +1,4 @@
-CORE
+CORE smt-backend
 invalid.c
 --trace --smt2 --z3
 ^EXIT=10$
diff --git a/regression/cbmc/z3/valid.desc b/regression/cbmc/z3/valid.desc
index ced8c4b6e56..ca634f915aa 100644
--- a/regression/cbmc/z3/valid.desc
+++ b/regression/cbmc/z3/valid.desc
@@ -1,4 +1,4 @@
-CORE
+CORE smt-backend
 valid.c
 --trace --smt2 --z3
 ^EXIT=0$