Nuno Lopes cc6769c866 improve bit-blasting for the case (bvsrem var power-of-two) ... We will now transform bvsrem into an extract + zero extend Gives ~40% speedup in selected benchmarks Signed-off-by: Nuno Lopes <nlopes@microsoft.com>		2016-02-01 13:46:55 +00:00
..
api	add a little more verbiage to description of simplify. Issue #424	2016-01-27 14:47:15 -08:00
ast	improve bit-blasting for the case (bvsrem var power-of-two)	2016-02-01 13:46:55 +00:00
cmd_context	fixing bugs in seq	2016-01-23 10:38:49 -05:00
duality	reworking cancellation	2015-12-12 19:30:23 +00:00
interp	issue #393 -- removed debugging assert	2016-01-04 12:53:46 -08:00
math	update re simplification	2016-01-15 10:11:39 +05:30
model	add seq_rewriter to model_evaluator, remove th_rewriter additional step in validator	2016-01-15 04:02:48 +05:30
muz	update display method for datalog to use predicates, throttle use of extensionality	2016-01-28 20:23:06 -08:00
nlsat	ensure limit children are safe for race conditions	2015-12-12 19:30:24 +00:00
opt	fix axioms for extract, add extensionality checking for shared variables, convert exceptions to unknown status per #419	2016-01-18 11:09:41 +05:30
parsers	make parse error a bit more informative	2016-01-19 19:09:41 +01:00
qe	updates to resource exceptions, update master possibly handle pull request issue	2015-12-12 11:36:49 -08:00
sat	fix axioms for extract, add extensionality checking for shared variables, convert exceptions to unknown status per #419	2016-01-18 11:09:41 +05:30
shell	remove unused decl	2015-12-30 15:50:46 +00:00
smt	update display method for datalog to use predicates, throttle use of extensionality	2016-01-28 20:23:06 -08:00
solver	fix bugs exposed by Chris' sequence unit tests. Improve diagnostics for reason-unknown in combined solver	2016-01-28 08:50:13 -08:00
tactic	Merge branch 'master' of https://github.com/Z3Prover/z3	2016-01-28 11:14:11 +00:00
test	resource-limit related fixes in src/test	2015-12-18 18:43:38 +00:00
util	remove unused exceeded_memory_allocations class	2016-01-27 18:09:24 +00:00