mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-26 09:24:36 +00:00
Code Activity
5451 commits 45 branches 52 tags 177 MiB
Commit graph

5451 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
32b6b2da44 moving to resource managed cancellation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-11 13:13:11 -08:00
Nikolaj Bjorner
61dbb6168e cleanup cancelation logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-11 12:35:35 -08:00
Christoph M. Wintersteiger
f164f17190 ocaml build fix 2015-12-11 20:01:55 +00:00
Christoph M. Wintersteiger
50f17e403c updated ocaml build and installation 2015-12-11 19:56:23 +00:00
Nuno Lopes
39ca5480d7 ensure that formula is skolemized in the smt solver when using MBQI 
Reviewed by Nikolaj

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-12-11 18:18:09 +00:00
Nuno Lopes
ef06da8c2c fix build with gcc 2015-12-11 18:14:14 +00:00
Christoph M. Wintersteiger
3388e1e628 Removed superfluous file. 2015-12-11 18:00:38 +00:00
Christoph M. Wintersteiger
8fef9e57c5 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-11 17:52:12 +00:00
Nikolaj Bjorner
4e155887b2 consolidate cancellation to context check_cancel_flag instead of calling in set_cancel() 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-11 09:51:43 -08:00
Christoph M. Wintersteiger
ea353d77e9 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-11 17:48:50 +00:00
Christoph M. Wintersteiger
12ee1d342c Improved argument validation in FP API. 
Fixes #372
 2015-12-11 17:48:40 +00:00
Nikolaj Bjorner
ee4ed1749a add cancel checks in model finder, patch by Sarah Winkler 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-11 09:09:25 -08:00
Nikolaj Bjorner
aa415f3d58 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-11 08:37:55 -08:00
Nikolaj Bjorner
85b9bb3cc6 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-11 08:37:47 -08:00
Christoph M. Wintersteiger
b25f517a89 Bugfix for C++ API. 
Fixes #371.
 2015-12-11 14:03:41 +00:00
Christoph M. Wintersteiger
cc8e685f45 whitespace 2015-12-11 14:03:24 +00:00
Nikolaj Bjorner
58411f64e8 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-10 20:25:12 -08:00
Nikolaj Bjorner
5eb23e1e7a seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-10 19:20:16 -08:00
Christoph M. Wintersteiger
383d06b225 Bugfix for Expr.isInt in .NET, Java, ML. 
Fixes #370
 2015-12-10 15:13:55 +00:00
Nikolaj Bjorner
30580a012a seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-10 02:38:56 -08:00
Nikolaj Bjorner
d81186eaca seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-10 01:36:17 -08:00
Nikolaj Bjorner
f9ca66d90b seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-09 23:19:16 -08:00
Nikolaj Bjorner
d58c219b54 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-09 22:18:02 -08:00
Nikolaj Bjorner
c5a9d81d93 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-09 20:17:00 -08:00
Nikolaj Bjorner
fe1039d12f seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-09 14:48:50 -08:00
Nikolaj Bjorner
0e701138e1 disable restart code in seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-09 09:53:18 -08:00
Nikolaj Bjorner
035f2bb0da disable unsound simplification of root objects, and incorrect evaluation of negative even roots 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-09 08:41:59 -08:00
Nikolaj Bjorner
8949790c16 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-09 07:37:51 -08:00
Nikolaj Bjorner
820fb10ef8 create .so impages for OpenBSD 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-09 07:37:40 -08:00
Nikolaj Bjorner
d11022cf2d Merge pull request #362 from NikolajBjorner/master 
Combined updates to seq, add openbsd cases to build script.
 2015-12-09 07:30:51 -08:00
Nikolaj Bjorner
b1a1aa5007 remove unused field 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-09 07:09:23 -08:00
Christoph M. Wintersteiger
a0eace4921 Merge branch 'delcypher-fix_recent_breakages2' 2015-12-09 13:07:57 +00:00
Christoph M. Wintersteiger
84291825e6 Resolved conflicts 2015-12-09 13:07:25 +00:00
Christoph M. Wintersteiger
a0f9f461f8 Build fix 2015-12-09 13:01:42 +00:00
Nuno Lopes
d9cd01f3f7 remove a few leftovers from min aggregation cleanup 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-12-09 09:28:17 +00:00
Nikolaj Bjorner
aebdc8950a Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-09 00:40:36 -08:00
Nikolaj Bjorner
b9302e6caf seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-09 00:38:03 -08:00
Nikolaj Bjorner
94bd2fdbe4 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-08 21:03:28 -08:00
Nikolaj Bjorner
24de0a9b90 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-08 16:37:08 -08:00
Nikolaj Bjorner
6c2e7e7675 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-08 16:03:24 -08:00
Dan Liew
0a1c645b5e Don't emit install commands and dependencies if ML bindings are 
disabled!
 2015-12-08 23:20:39 +00:00
Dan Liew
edf5ed27df Attempt to allow (but warn about) installation of Python bindings 
under OSX when the Python ``site-packages`` directory doesn't live
under the install prefix. Also disallow installing under Windows
as it doesn't really make sense.
 2015-12-08 23:10:48 +00:00
Dan Liew
d98d392aac Try unbreak OSX build when Python installation doesn't live under 
PREFIX. In this case it is not safe to call ``strip_path_prefix()``
due to the assertion error it will raise.
 2015-12-08 23:10:48 +00:00
Dan Liew
0a8cd3ae19 Refactor the install and uninstall commands for the python bindings 
out of ``DLLComponent`` and into ``PythonInstallComponent`` where they
belong.
 2015-12-08 23:10:48 +00:00
Dan Liew
38b45919b5 Unbreak running `make install. The python site-package` directory 
was not created before trying to create files in it.

The ``install_deps()`` method was also dead. It looks like that
should have been named ``mk_install_deps()`` but even if we give it
the right name it does the wrong thing. That method is supposed
emit target names (i.e. dependencies) not commands.
 2015-12-08 23:10:48 +00:00
Dan Liew
e2546d2b95 Refactor references to `pythonPkgDirWithoutPrefix` to a object 
attribute.
 2015-12-08 23:08:23 +00:00
Nikolaj Bjorner
932a3a8387 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-08 13:27:17 -08:00
Christoph M. Wintersteiger
83db19654f refactored ocamlfind_install target 2015-12-08 18:57:17 +00:00
Nikolaj Bjorner
895d032996 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-08 10:33:09 -08:00
Nuno Lopes
4b0f2cae0d fix compiler warning in scoped_timer.cpp on linux 
2 secs in nanosec representation still fit in 31 bits, so no need for ULL

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-12-08 17:03:18 +00:00