mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Enable more tests on non-Windows. (#6199)
Some tests were `#ifdef _WINDOWS` even though they compiled and ran on other platforms. Remove the #ifdef protections in these cases.
This commit is contained in:
parent
44100a3a08
commit
78237578f3
|
@ -4,7 +4,6 @@ Copyright (c) 2015 Microsoft Corporation
|
|||
|
||||
--*/
|
||||
|
||||
#ifdef _WINDOWS
|
||||
#include "api/z3.h"
|
||||
#include "api/z3_private.h"
|
||||
#include <iostream>
|
||||
|
@ -112,7 +111,3 @@ void tst_api() {
|
|||
test_bvneg();
|
||||
test_mk_distinct();
|
||||
}
|
||||
#else
|
||||
void tst_api() {
|
||||
}
|
||||
#endif
|
||||
|
|
|
@ -4,7 +4,6 @@ Copyright (c) 2015 Microsoft Corporation
|
|||
|
||||
--*/
|
||||
|
||||
#ifdef _WINDOWS
|
||||
#include "ast/reg_decl_plugins.h"
|
||||
#include "muz/base/dl_context.h"
|
||||
#include "muz/fp/dl_register_engine.h"
|
||||
|
@ -362,7 +361,3 @@ void tst_dl_product_relation() {
|
|||
test_finite_product_relation(fparams, params);
|
||||
|
||||
}
|
||||
#else
|
||||
void tst_dl_product_relation() {
|
||||
}
|
||||
#endif
|
||||
|
|
|
@ -4,8 +4,6 @@ Copyright (c) 2015 Microsoft Corporation
|
|||
|
||||
--*/
|
||||
|
||||
#ifdef _WINDOWS
|
||||
|
||||
#include "ast/reg_decl_plugins.h"
|
||||
#include "muz/base/dl_context.h"
|
||||
#include "muz/fp/dl_register_engine.h"
|
||||
|
@ -296,8 +294,3 @@ void tst_dl_relation() {
|
|||
datalog::test_interval_relation();
|
||||
datalog::test_bound_relation();
|
||||
}
|
||||
|
||||
#else
|
||||
void tst_dl_relation() {
|
||||
}
|
||||
#endif
|
||||
|
|
|
@ -16,7 +16,6 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifdef _WINDOWS
|
||||
#include "ast/substitution/matcher.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/reg_decl_plugins.h"
|
||||
|
@ -110,7 +109,3 @@ void tst1() {
|
|||
void tst_matcher() {
|
||||
tst1();
|
||||
}
|
||||
#else
|
||||
void tst_matcher() {
|
||||
}
|
||||
#endif
|
||||
|
|
|
@ -4,7 +4,6 @@ Copyright (c) 2015 Microsoft Corporation
|
|||
|
||||
--*/
|
||||
|
||||
#ifdef _WINDOWS
|
||||
#include "api/z3.h"
|
||||
#include "api/z3_private.h"
|
||||
#include <iostream>
|
||||
|
@ -59,8 +58,3 @@ void tst_memory() {
|
|||
Z3_reset_memory();
|
||||
|
||||
}
|
||||
|
||||
#else
|
||||
void tst_memory() {
|
||||
}
|
||||
#endif
|
||||
|
|
|
@ -16,7 +16,6 @@ Author:
|
|||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifdef _WINDOWS
|
||||
|
||||
#include "api/z3.h"
|
||||
#include "util/trace.h"
|
||||
|
@ -724,7 +723,3 @@ void tst_no_overflow() {
|
|||
}
|
||||
}
|
||||
}
|
||||
#else
|
||||
void tst_no_overflow() {
|
||||
}
|
||||
#endif
|
||||
|
|
|
@ -4,7 +4,6 @@ Copyright (c) 2015 Microsoft Corporation
|
|||
|
||||
--*/
|
||||
|
||||
#ifdef _WINDOWS
|
||||
#include "api/z3.h"
|
||||
#include "api/z3_private.h"
|
||||
#include <iostream>
|
||||
|
@ -214,8 +213,3 @@ void tst_simplifier() {
|
|||
test_bool();
|
||||
test_skolemize_bug();
|
||||
}
|
||||
|
||||
#else
|
||||
void tst_simplifier() {
|
||||
}
|
||||
#endif
|
||||
|
|
Loading…
Reference in a new issue