3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
z3/src
2017-05-03 17:46:06 -04:00
..
ackermannization Adding translation to ackr_model_converter. 2016-06-06 18:06:45 +01:00
api Merge pull request #984 from delcypher/cmake_doxygen 2017-04-27 06:58:32 -07:00
ast cleanup 2017-05-03 17:45:56 -04:00
cmd_context deal with subtraction that manages to sneak in. Issue #996 2017-05-01 15:22:06 -07:00
duality Added rewriter.ignore_patterns_on_ground_qbody option to disable simplification of quantifiers that have their universals appear only in patterns, but otherwise have a ground body. 2017-04-07 21:19:20 +01:00
interp update license for space/quotes per #982 2017-04-24 13:34:10 -07:00
math remove polynomial factorization as suggested by issue #852 2017-01-09 21:30:54 -08:00
model ensure evaluation of array equalities is enabled for external facing evaluator. Issue #917 2017-03-09 05:29:56 +01:00
muz include 'stopwatch.h' to avoid ODR warnings, #994 2017-04-30 11:28:11 -07:00
nlsat fixing unsat core extraction for tactics 2016-11-02 14:14:55 +00:00
opt update to retain original behavior 2017-05-02 19:32:03 -07:00
parsers cleanup 2017-05-03 17:45:56 -04:00
qe Added rewriter.ignore_patterns_on_ground_qbody option to disable simplification of quantifiers that have their universals appear only in patterns, but otherwise have a ground body. 2017-04-07 21:19:20 +01:00
sat fix quadratic behavior of extract_assumptions 2017-05-02 15:57:31 -07:00
shell renmae to opt_stream_buffer to avoid clash with dimacs stream buffer. #994 2017-04-30 12:54:29 -07:00
smt fix overlap detection internalization 2017-05-03 17:46:06 -04:00
solver smt_setup framework, all hooks to theory_str are redirected to theory_seq 2017-05-02 17:16:35 -04:00
tactic deal with subtraction that manages to sneak in. Issue #996 2017-05-01 15:22:06 -07:00
test Merge branch 'upstream-master' into develop 2017-05-03 17:03:13 -04:00
util Merge branch 'upstream-master' into develop 2017-04-04 16:47:30 -04:00