Nikolaj Bjorner 8e5dec882b Merge branch 'master' of https://github.com/Z3Prover/z3		2015-12-03 10:01:41 -08:00
..
api	C API cleanup. Mainly removal of ML-specific macros that are not used anymore and inline documentation fixes.	2015-12-03 17:33:25 +00:00
ast	Bugfix for FPA float to float conversion.	2015-11-24 17:21:40 +00:00
cmd_context	add some of the SMT2.5 features	2015-12-02 19:14:47 -08:00
duality	add macro for converting std::vectors to pointers (leaking abstraction)	2015-12-01 16:35:03 -08:00
interp	fix merge conflicts	2015-10-28 16:09:46 -07:00
math	Make Groebner basis computation interruptable. Exponsed in issue #269	2015-10-28 11:39:59 -07:00
model	fix rewriter for model validation	2015-11-03 07:45:42 -08:00
muz	bind variables in queries generated from Horn tactic to enforce that rule formulas don't contain free variables. Issue #328	2015-12-01 14:47:33 -08:00
nlsat	include rlimit in nlsat, include dedicated error message, for issue #216	2015-09-29 09:16:46 -07:00
opt	fix build with gcc	2015-11-22 11:24:30 +00:00
parsers	parsing of SMT 2.5 style string literals	2015-12-03 09:46:18 -08:00
qe	fix unintialized memory read exposed by nightly build	2015-09-06 14:15:08 -07:00
sat	disable aig tactic in inc_sat_solver (it can blow up the size of formulas significantly without sharing) and fix configuration update bug for optimization context exposed in example by Corina	2015-11-20 14:34:31 -08:00
shell	Trailing whitespace removed.	2015-11-03 12:28:10 +00:00
smt	fix leak in asserted_formulas::propagate_values() for proof generation mode	2015-11-29 10:49:52 +00:00
solver	working on Forking/Serializing a z3 Solver #209	2015-11-06 17:29:24 -08:00
tactic	Fix for #343. Optimizations introduced on 8-10-2015 were too agressive. Remove unreferened variable	2015-12-01 13:43:47 -08:00
test	fix tests	2015-11-20 08:00:01 -08:00
util	add macro for converting std::vectors to pointers (leaking abstraction)	2015-12-01 16:35:03 -08:00