Christoph M. Wintersteiger 2e362aa6c0 build fix		2016-07-29 01:02:48 +01:00
..
ackermannization	Adding translation to ackr_model_converter.	2016-06-06 18:06:45 +01:00
api	Merge branch 'master' of https://github.com/Z3Prover/z3	2016-07-28 11:20:23 -07:00
ast	added symbolic automata complement for sequences	2016-07-28 13:50:05 -07:00
cmd_context	set solver on simplify command	2016-07-27 15:35:44 -07:00
duality	fix warnings for unused variables	2016-05-17 13:54:22 -07:00
interp	fix build failures under linux	2016-07-09 13:28:39 -07:00
math	build fix	2016-07-29 01:02:48 +01:00
model	move arithmetical mbp functionality to model_based_opt	2016-06-26 16:12:14 -07:00
muz	have the classifier revert to full arithmetic on non-difference logic, reported on http://stackoverflow.com/questions/38594208/changing-order-of-z3-fixepoint-queries-changes-the-result/38596187#3	2016-07-26 10:32:54 -07:00
nlsat	fix bugs exposed in #677. to_int(x) has the semantics that to_int(x) <= x, and to_int(x) is the largest integer satisfying this inequality. The encoding in purify_arith had it the other way x <= to_int(x) contrary to how to_int(x) is handled elsewhere. Another bug in theory_arith for mixed-integer linear case was also exposed. Fractional bounds on expressions of the form to_int(x), and more generally on integer rows were not rounded prior to internalization	2016-07-13 20:32:18 -07:00
opt	updating default solver selection. Add dt2bv transformation	2016-07-24 18:16:32 -07:00
parsers	Merge branch 'master' of https://github.com/Z3Prover/z3	2016-06-14 08:10:21 -07:00
qe	move arithmetical mbp functionality to model_based_opt	2016-06-26 16:12:14 -07:00
sat	remove stale SLS option	2016-07-21 18:18:42 -07:00
shell	Added 32/64 bit indication and githash to output of -version.	2016-07-26 19:21:50 +01:00
smt	fast path for antecedent extraction in smt_context	2016-07-28 16:49:19 -07:00
solver	fast path for antecedent extraction in smt_context	2016-07-28 16:49:19 -07:00
tactic	adding support for distinct for dt2bv, re-entry harness for ~Context	2016-07-27 09:02:56 -07:00
test	adding hash/eq to uint_set	2016-07-27 13:41:41 -07:00
util	Merge branch 'master' of https://github.com/Z3Prover/z3	2016-07-28 18:07:48 +01:00