From 96e871c826fe7708ca8cd0061d38599bdcbe5bed Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 12 Dec 2021 12:31:15 -0800
Subject: [PATCH] add stub for testing updates to scoped_timer

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/seq_decl_plugin.cpp | 3 ++-
 src/test/CMakeLists.txt     | 1 +
 src/test/main.cpp           | 1 +
 src/test/scoped_timer.cpp   | 9 +++++++++
 4 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 src/test/scoped_timer.cpp

diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 8be046fd9..1e87e1402 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -416,7 +416,7 @@ func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
     case OP_RE_DERIVATIVE:
     case _OP_RE_ANTIMIROV_UNION:
         m_has_re = true;
-        // fall-through
+        Z3_fallthrough;   
     case OP_SEQ_UNIT:
     case OP_STRING_ITOS:
     case OP_STRING_STOI:
@@ -516,6 +516,7 @@ func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
     case OP_SEQ_REPLACE_RE_ALL:
     case OP_SEQ_REPLACE_RE:
         m_has_re = true;
+        Z3_fallthrough;
     case OP_SEQ_REPLACE_ALL:
         return mk_str_fun(k, arity, domain, range, k);        
 
diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
index eb0e94173..500cb4258 100644
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@@ -101,6 +101,7 @@ add_executable(test-z3
   sat_local_search.cpp
   sat_lookahead.cpp
   sat_user_scope.cpp
+  scoped_timer.cpp
   simple_parser.cpp
   simplex.cpp
   simplifier.cpp
diff --git a/src/test/main.cpp b/src/test/main.cpp
index 3e3f1d575..6272c2dee 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -259,6 +259,7 @@ int main(int argc, char ** argv) {
     TST(bdd);
     TST(pdd);
     TST(pdd_solver);
+    TST(scoped_timer);
     TST(solver_pool);
     //TST_ARGV(hs);
     TST(finder);
diff --git a/src/test/scoped_timer.cpp b/src/test/scoped_timer.cpp
new file mode 100644
index 000000000..c21e39cbe
--- /dev/null
+++ b/src/test/scoped_timer.cpp
@@ -0,0 +1,9 @@
+// test driver for scoped timer.
+// fixes are required to be fuzzed
+// with single and multi-threaded mode and short timeouts.
+
+#include "util/scoped_timer.h"
+
+void tst_scoped_timer() {
+    
+}