mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 04:03:39 +00:00
add stub for testing updates to scoped_timer
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
0405a597d4
commit
96e871c826
|
@ -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_DERIVATIVE:
|
||||||
case _OP_RE_ANTIMIROV_UNION:
|
case _OP_RE_ANTIMIROV_UNION:
|
||||||
m_has_re = true;
|
m_has_re = true;
|
||||||
// fall-through
|
Z3_fallthrough;
|
||||||
case OP_SEQ_UNIT:
|
case OP_SEQ_UNIT:
|
||||||
case OP_STRING_ITOS:
|
case OP_STRING_ITOS:
|
||||||
case OP_STRING_STOI:
|
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_ALL:
|
||||||
case OP_SEQ_REPLACE_RE:
|
case OP_SEQ_REPLACE_RE:
|
||||||
m_has_re = true;
|
m_has_re = true;
|
||||||
|
Z3_fallthrough;
|
||||||
case OP_SEQ_REPLACE_ALL:
|
case OP_SEQ_REPLACE_ALL:
|
||||||
return mk_str_fun(k, arity, domain, range, k);
|
return mk_str_fun(k, arity, domain, range, k);
|
||||||
|
|
||||||
|
|
|
@ -101,6 +101,7 @@ add_executable(test-z3
|
||||||
sat_local_search.cpp
|
sat_local_search.cpp
|
||||||
sat_lookahead.cpp
|
sat_lookahead.cpp
|
||||||
sat_user_scope.cpp
|
sat_user_scope.cpp
|
||||||
|
scoped_timer.cpp
|
||||||
simple_parser.cpp
|
simple_parser.cpp
|
||||||
simplex.cpp
|
simplex.cpp
|
||||||
simplifier.cpp
|
simplifier.cpp
|
||||||
|
|
|
@ -259,6 +259,7 @@ int main(int argc, char ** argv) {
|
||||||
TST(bdd);
|
TST(bdd);
|
||||||
TST(pdd);
|
TST(pdd);
|
||||||
TST(pdd_solver);
|
TST(pdd_solver);
|
||||||
|
TST(scoped_timer);
|
||||||
TST(solver_pool);
|
TST(solver_pool);
|
||||||
//TST_ARGV(hs);
|
//TST_ARGV(hs);
|
||||||
TST(finder);
|
TST(finder);
|
||||||
|
|
9
src/test/scoped_timer.cpp
Normal file
9
src/test/scoped_timer.cpp
Normal file
|
@ -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() {
|
||||||
|
|
||||||
|
}
|
Loading…
Reference in a new issue