mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 09:05:31 +00:00
add unit test stub
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c629f09f21
commit
b8493e9a57
3 changed files with 17 additions and 0 deletions
|
@ -89,6 +89,7 @@ add_executable(test-z3
|
|||
permutation.cpp
|
||||
polynomial.cpp
|
||||
polynorm.cpp
|
||||
polysat.cpp
|
||||
prime_generator.cpp
|
||||
proof_checker.cpp
|
||||
qe_arith.cpp
|
||||
|
|
|
@ -262,4 +262,5 @@ int main(int argc, char ** argv) {
|
|||
TST(solver_pool);
|
||||
//TST_ARGV(hs);
|
||||
TST(finder);
|
||||
TST(polysat);
|
||||
}
|
||||
|
|
15
src/test/polysat.cpp
Normal file
15
src/test/polysat.cpp
Normal file
|
@ -0,0 +1,15 @@
|
|||
#include "math/polysat/polysat.h"
|
||||
|
||||
namespace polysat {
|
||||
// test resolve, factoring routines
|
||||
// auxiliary
|
||||
static void test1() {
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
// also add test that loads from a file and runs the polysat engine.
|
||||
|
||||
void tst_polysat() {
|
||||
polysat::test1();
|
||||
}
|
Loading…
Add table
Add a link
Reference in a new issue