3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 22:05:36 +00:00
z3/src/test
Nikolaj Bjorner 64f3b3e316 remove lp_main from test branch to ensure test build only builds a single entry point
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-12 07:59:16 -07:00
..
fuzzing remove sources for unused variable warnings 2016-12-21 09:54:45 -08:00
algebraic.cpp resource-limit related fixes in src/test 2015-12-18 18:43:38 +00:00
api.cpp fix tests 2015-11-20 08:00:01 -08:00
api_bug.cpp fix tests 2015-11-20 08:00:01 -08:00
argument_parser.h missing files 2017-05-09 14:14:58 -07:00
arith_rewriter.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
arith_simplifier_plugin.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
ast.cpp add hilbert basis utility for extracting auxiliary invariants 2013-02-12 14:58:04 -08:00
bit_blaster.cpp checkpoint 2012-10-21 22:16:58 -07:00
bit_vector.cpp add unit test for previous commit 2013-03-22 11:51:28 -07:00
bits.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
buffer.cpp checkpoint 2012-10-21 22:16:58 -07:00
bv_simplifier_plugin.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
chashtable.cpp checkpoint 2012-10-21 22:16:58 -07:00
check_assumptions.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
cnf_backbones.cpp update to retain original behavior 2017-05-02 19:30:54 -07:00
datalog_parser.cpp fix unit test for datalog parser, fixes issue #224 2015-09-28 11:16:55 -07:00
ddnf.cpp tuning and fixing consequence finding, adding dimacs evaluation 2017-04-26 13:53:37 -07:00
diff_logic.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
dl_context.cpp comment out unit test that depends on hard-wired path 2015-10-04 16:34:23 -07:00
dl_product_relation.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
dl_query.cpp disable code in dl_query that depends on hard-wired file path 2015-10-03 17:30:12 -07:00
dl_relation.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
dl_table.cpp remove a few leftovers from min aggregation cleanup 2015-12-09 09:28:17 +00:00
dl_util.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
doc.cpp eliminated unused variable 2015-10-04 15:16:41 +01:00
escaped.cpp checkpoint 2012-10-21 22:16:58 -07:00
ex.cpp fix unit test for default exception 2015-07-06 22:52:44 -07:00
expr_rand.cpp fix test build, working on rec-functions and automata complementation 2016-03-01 22:31:44 -08:00
expr_substitution.cpp comment out diverging portion of unit test. Issue #210 2015-10-04 11:24:22 -07:00
ext_numeral.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
f2n.cpp checkpoint 2012-10-21 22:16:58 -07:00
factor_rewriter.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
fixed_bit_vector.cpp fix overflow bugs in doc 2014-09-22 22:03:59 -07:00
for_each_file.cpp checkpoint 2012-10-21 22:16:58 -07:00
for_each_file.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00
get_consequences.cpp remove legacy interface to dt2bv tactic 2016-10-18 23:04:17 -04:00
get_implied_equalities.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
hashtable.cpp Fixed #include of <hash_set> which is deprecated in VS2015 and will be removed. 2015-10-27 17:11:40 +00:00
heap.cpp checkpoint 2012-10-21 22:16:58 -07:00
heap_trie.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
hilbert_basis.cpp resource-limit related fixes in src/test 2015-12-18 18:43:38 +00:00
horn_subsume_model_converter.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
hwf.cpp Fixed warnings reported by gcc 4.7.1 2012-10-31 00:16:26 -07:00
im_float_config.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00
inf_rational.cpp Fixed warnings produced by gcc 4.6.3 when compiling in debug mode 2012-10-30 23:43:00 -07:00
interval.cpp resource-limit related fixes in src/test 2015-12-18 18:43:38 +00:00
karr.cpp resource-limit related fixes in src/test 2015-12-18 18:43:38 +00:00
list.cpp checkpoint 2012-10-21 22:16:58 -07:00
lp.cpp convert static random fields to non-static 2017-05-11 16:46:07 -07:00
main.cpp merge LRA 2017-05-09 10:46:11 -07:00
map.cpp fixing some compilation warnings 2012-10-24 23:43:58 -07:00
matcher.cpp fix a few compilation warnings 2013-04-21 14:36:39 -07:00
memory.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
model2expr.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
model_based_opt.cpp move arithmetical mbp functionality to model_based_opt 2016-06-26 14:30:35 -07:00
model_evaluator.cpp use std::vector per Nuno's analysis to fix #420 2016-03-07 08:08:17 -08:00
model_retrieval.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
mpbq.cpp checkpoint 2012-10-21 22:16:58 -07:00
mpf.cpp checkpoint 2012-10-21 22:16:58 -07:00
mpff.cpp Update mpff.cpp to fix build with clang and new gcc 2016-09-26 08:05:15 +02:00
mpfx.cpp checkpoint 2012-10-21 22:16:58 -07:00
mpq.cpp Fixed warnings reported by gcc 4.7.1 2012-10-31 00:05:38 -07:00
mpz.cpp fix build with new gcc and clang compilers 2016-09-26 08:06:38 +02:00
nlarith_util.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
nlsat.cpp moving remaining qsat functionality over 2016-03-19 15:35:26 -07:00
no_overflow.cpp fix tests 2015-11-20 08:00:01 -08:00
object_allocator.cpp Fixed warnings produced by gcc 4.6.3 when compiling in debug mode 2012-10-30 23:43:00 -07:00
old_interval.cpp Eliminated unused variable 2015-10-04 15:51:27 +01:00
optional.cpp checkpoint 2012-10-21 22:16:58 -07:00
parray.cpp Fixed warnings produced by gcc 4.6.3 when compiling in debug mode 2012-10-30 23:43:00 -07:00
pb2bv.cpp add bounded-int and pb2bv solvers to fd_solver, use sorting networks for pb2bv rewriter when applicable, hoist to pb2bv_rewriter module and remove it from the pb2bv_tactic 2016-10-23 20:31:59 -07:00
pdr.cpp deal with unit test failure cases, fixes #132 #133 2015-06-17 17:30:10 -07:00
permutation.cpp fixed more compilation errors reported by g++ 4.7.1 2012-10-27 22:32:50 -07:00
polynomial.cpp Removed polynomial factorization test cases. Relates to #852 and fixes #865. 2017-01-10 14:02:59 +00:00
polynorm.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
prime_generator.cpp checkpoint 2012-10-21 22:16:58 -07:00
proof_checker.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
qe_arith.cpp fixed unhandled case warning in test/qe_arith.cpp 2016-10-25 14:34:00 +01:00
quant_elim.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
quant_solve.cpp disable memory finalization after quant_solve unit test. Related to issue #210 2015-10-03 17:37:33 -07:00
random.cpp checkpoint 2012-10-21 22:16:58 -07:00
rational.cpp Fix is_int64 bug in mpz when compiling with GMP 2013-04-08 14:50:17 -07:00
rcf.cpp resource-limit related fixes in src/test 2015-12-18 18:43:38 +00:00
region.cpp checkpoint 2012-10-21 22:16:58 -07:00
sat_user_scope.cpp Propagated rlimit changes to sat::solver into sat_user_scope tests 2015-09-29 11:50:10 +01:00
simple_parser.cpp Isolating reg_decl_plugins 2012-10-24 11:27:50 -07:00
simplex.cpp resource-limit related fixes in src/test 2015-12-18 18:43:38 +00:00
simplifier.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
small_object_allocator.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
smt2print_parse.cpp Merge branch 'develop' into upstream-master 2016-06-01 17:40:52 -04:00
smt_context.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
smt_reader.h fix build issues part 3 2017-05-11 07:49:41 -07:00
sorting_network.cpp build fix 2016-11-01 11:23:42 +00:00
stack.cpp checkpoint 2012-10-21 22:16:58 -07:00
string_buffer.cpp checkpoint 2012-10-21 22:16:58 -07:00
substitution.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
symbol.cpp checkpoint 2012-10-21 22:16:58 -07:00
symbol_table.cpp checkpoint 2012-10-21 22:16:58 -07:00
tbv.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
test_file_reader.h missing files 2017-05-09 14:14:58 -07:00
test_util.h added missing Copyright forms 2015-06-10 11:54:02 -07:00
theory_dl.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
theory_pb.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
timeout.cpp added missing Copyright forms 2015-06-10 11:54:02 -07:00
total_order.cpp checkpoint 2012-10-21 22:16:58 -07:00
trigo.cpp resource-limit related fixes in src/test 2015-12-18 18:43:38 +00:00
udoc_relation.cpp Fixed a bug in udoc_relation's join project 2015-06-17 17:14:23 +01:00
uint_set.cpp adding hash/eq to uint_set 2016-07-27 13:41:41 -07:00
upolynomial.cpp resource-limit related fixes in src/test 2015-12-18 18:43:38 +00:00
var_subst.cpp updating tests 2013-02-12 18:13:02 -08:00
vector.cpp Adding overflow checks 2013-09-02 19:43:22 -07:00