Christoph M. Wintersteiger 7a2a2a32cc Merge branch 'master' of https://github.com/Z3Prover/z3		2018-10-01 17:25:14 +01:00
..
ackermannization	remove spurious copies and inc_refs around ref_vector	2018-06-28 10:31:38 +01:00
api	Merge branch 'master' of https://github.com/z3prover/z3	2018-10-01 09:18:46 -07:00
ast	Follow-up fix for fpa2bv_converter.	2018-10-01 17:25:02 +01:00
cmd_context	fix include path for z3_version.h	2018-09-21 20:30:50 -07:00
math	force the new arithmetic solver for QF_LIA	2018-07-09 16:33:48 -07:00
model	visit parameters during occurs count	2018-06-29 08:52:25 -07:00
muz	Fix is_infty_level to treat 2^16-1 as infinity	2018-09-04 21:49:59 -04:00
nlsat	strengthen filter for specialized tactic conditions, add flag to disable hnf to lp_params	2018-07-15 22:35:47 -07:00
opt	purify non-constant terms by default to enforce theory #1820	2018-09-10 15:52:02 -07:00
parsers	remove some allocs from exceptions	2018-07-02 17:08:02 +01:00
qe	add capabilities to python API, fix model extraction for qsat	2018-09-28 13:23:28 -07:00
sat	add psat to available tactics	2018-09-30 17:44:28 -07:00
shell	rename version.h to z3_version.h to differentiate name in install include directory. Add support for z3_version.h in python build system. #1833	2018-09-21 20:13:58 -07:00
smt	fix sort retrieval for lambdas	2018-10-01 09:18:40 -07:00
solver	pop to base before incremental internalization to ensure that units are not lost	2018-09-22 14:04:15 -07:00
tactic	fix #1783, wronge clausification of negated pb inequalities. Signs were ignored	2018-08-11 13:33:09 -07:00
test	fix test build	2018-09-20 18:57:47 -07:00
util	Fixed filename in CMakeLists.txt	2018-10-01 12:29:14 +01:00
CMakeLists.txt	rename version.h to z3_version.h to differentiate name in install include directory. Add support for z3_version.h in python build system. #1833	2018-09-21 20:13:58 -07:00