3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
z3/src/test
Nikolaj Bjorner 1733af2641 test case for non-termination of substitution/rewriting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-09-24 05:33:16 +03:00
..
fuzzing Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id 2012-12-18 17:14:25 -08:00
algebraic.cpp Fix typos and bugs. Add tests. 2013-01-04 15:01:27 -08:00
api.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
api_bug.cpp checkpoint 2012-10-23 12:12:59 -07:00
arith_rewriter.cpp add normalizer of monomial coefficients 2013-08-10 10:50:03 -07:00
arith_simplifier_plugin.cpp removed front-end-params 2012-12-02 10:05:29 -08: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 checkpoint 2012-10-21 22:16:58 -07:00
buffer.cpp checkpoint 2012-10-21 22:16:58 -07:00
bv_simplifier_plugin.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
chashtable.cpp checkpoint 2012-10-21 22:16:58 -07:00
check_assumptions.cpp removed front-end-params 2012-12-02 10:05:29 -08:00
datalog_parser.cpp re-organize muz_qe into separate units 2013-08-28 21:20:24 -07:00
diff_logic.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
dl_context.cpp re-organize muz_qe into separate units 2013-08-28 21:20:24 -07:00
dl_product_relation.cpp re-organize muz_qe into separate units 2013-08-28 21:20:24 -07:00
dl_query.cpp re-organize muz_qe into separate units 2013-08-28 21:20:24 -07:00
dl_relation.cpp re-organize muz_qe into separate units 2013-08-28 21:20:24 -07:00
dl_table.cpp re-organize muz_qe into separate units 2013-08-28 21:20:24 -07:00
dl_util.cpp checkpoint 2012-10-21 22:16:58 -07:00
escaped.cpp checkpoint 2012-10-21 22:16:58 -07:00
ex.cpp checkpoint 2012-10-21 22:16:58 -07:00
expr_rand.cpp Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id 2012-12-18 17:14:25 -08:00
expr_substitution.cpp test case for non-termination of substitution/rewriting 2013-09-24 05:33:16 +03: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 Isolating reg_decl_plugins 2012-10-24 11:27:50 -07:00
for_each_file.cpp checkpoint 2012-10-21 22:16:58 -07:00
for_each_file.h checkpoint 2012-10-21 22:16:58 -07:00
get_implied_equalities.cpp fix get_implied equalities and the unit test 2012-12-11 21:39:31 -08:00
hashtable.cpp checkpoint 2012-10-21 22:16:58 -07:00
heap.cpp checkpoint 2012-10-21 22:16:58 -07:00
heap_trie.cpp test hilbert-basis with fdds and checked integers 2013-03-26 17:31:11 -07:00
hilbert_basis.cpp fix compiler warnings and errors 2013-04-03 17:03:07 -07:00
horn_subsume_model_converter.cpp Isolating reg_decl_plugins 2012-10-24 11:27:50 -07:00
hwf.cpp Fixed warnings reported by gcc 4.7.1 2012-10-31 00:16:26 -07:00
im_float_config.h checkpoint 2012-10-21 22:16:58 -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 Fixed warnings reported by gcc 4.7.1 2012-10-31 00:05:38 -07:00
karr.cpp fix compiler warnings and errors 2013-04-03 17:03:07 -07:00
list.cpp checkpoint 2012-10-21 22:16:58 -07:00
main.cpp add test case for substitution 2013-09-24 05:13:11 +03: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 compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
model2expr.cpp Isolating reg_decl_plugins 2012-10-24 11:27:50 -07:00
model_retrieval.cpp Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id 2012-12-18 17:14:25 -08: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 Fixed warnings reported by gcc 4.7.1 2012-10-31 00:05:38 -07: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 Fixed warnings reported by gcc 4.7.1 2012-10-31 00:05:38 -07:00
nlarith_util.cpp Isolating reg_decl_plugins 2012-10-24 11:27:50 -07:00
nlsat.cpp Fixed warnings produced by gcc 4.6.3 when compiling in debug mode 2012-10-30 23:43:00 -07:00
no_overflow.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07: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 checkpoint 2012-10-21 22:16:58 -07: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
permutation.cpp fixed more compilation errors reported by g++ 4.7.1 2012-10-27 22:32:50 -07:00
polynomial.cpp Added support for clang++ on OSX 2012-11-12 04:56:48 +00:00
polynomial_factorization.cpp Fixed warnings reported by gcc 4.7.1 2012-10-31 00:05:38 -07:00
polynorm.cpp more on polynorm 2013-08-14 11:55:23 -07:00
prime_generator.cpp checkpoint 2012-10-21 22:16:58 -07:00
proof_checker.cpp checkpoint 2012-10-21 22:16:58 -07:00
qe_arith.cpp Fix build of test 2013-09-15 04:24:20 -07:00
quant_elim.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
quant_solve.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -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 Fix memory allocation problems in RCF module 2013-04-10 19:03:25 -07:00
region.cpp checkpoint 2012-10-21 22:16:58 -07:00
simple_parser.cpp Isolating reg_decl_plugins 2012-10-24 11:27:50 -07:00
simplifier.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
small_object_allocator.cpp checkpoint 2012-10-21 22:16:58 -07:00
smt2print_parse.cpp checkpoint 2012-10-21 22:16:58 -07:00
smt_context.cpp removed front-end-params 2012-12-02 10:05:29 -08: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 update substitution routines 2013-01-21 21:59:20 -08:00
symbol.cpp checkpoint 2012-10-21 22:16:58 -07:00
symbol_table.cpp checkpoint 2012-10-21 22:16:58 -07:00
test_util.h checkpoint 2012-10-21 22:16:58 -07:00
theory_dl.cpp removed front-end-params 2012-12-02 10:05:29 -08:00
timeout.cpp checkpoint 2012-10-23 12:12:59 -07:00
total_order.cpp checkpoint 2012-10-21 22:16:58 -07:00
trigo.cpp Fixed warnings reported by gcc 4.7.1 2012-10-31 00:05:38 -07:00
uint_set.cpp checkpoint 2012-10-21 22:16:58 -07:00
upolynomial.cpp Fixed warnings reported by gcc 4.7.1 2012-10-31 00:05:38 -07: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