3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Commit graph

474 commits

Author SHA1 Message Date
Nikolaj Bjorner
6558999cef fixes #1171
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-27 08:46:20 -07:00
Nikolaj Bjorner
b1298d7bde ensure that assertions within the unit tests are exercised in all build modes, remove special handling of SASSERT for release mode #1163
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-26 20:28:55 -07:00
Nikolaj Bjorner
9f9c575451 fix bug exposed when running test-z3.exe /a in debug mode, #1159. Add assertions to heap interaction
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-25 16:26:45 -07:00
Nikolaj Bjorner
70f6280bf1 fix regression reported in #1159
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-25 10:18:21 -07:00
Nikolaj Bjorner
a94f5fb04a fix compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-24 12:15:10 -07:00
Nikolaj Bjorner
253870c6d7 fix compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-04 13:08:23 -07:00
Nikolaj Bjorner
031d7e1b59 use iterators, update build icon for osx
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-01 16:58:40 -07:00
Lev Nachmanson
dfe15adf7e fix maybe non initialized warning
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2017-06-26 16:32:44 -07:00
Nikolaj Bjorner
7db1847f51 fix bitrot in maxsat example reference management #1116
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-26 09:36:53 -07:00
Christoph M. Wintersteiger
2fceac04d4 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-06-25 22:19:54 +01:00
Christoph M. Wintersteiger
c395516058 Adjusted rlimit increments in theory_arith to avoid non-termination issues 2017-06-25 22:19:42 +01:00
Lev Nachmanson
2a5f1d6e93 add a template instantination
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2017-06-22 10:32:35 -07:00
Dan Liew
d00892c9a6 [CMake] Fix dependencies for generating mem_initializer.cpp.
Previously CMake was not aware of which headers files the generation
of `mem_initializer.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declare memory initializers/finalizers change.
* New headers are added that declare memory initializers/finalizer.

Now the `z3_add_component()` CMake function has been modifed so that
it now takes an optional `MEMORY_INIT_FINALIZER_HEADERS` argument
which allows the headers that declare memory initializers/finalizers
to be explicitly listed.

With this information CMake will now regenerate `mem_initializer.cpp`
correctly.

This required the `mk_mem_initializer_cpp_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
2017-06-21 23:56:53 +01:00
Dan Liew
6f48a145aa [CMake] Fix dependencies for generating gparams_register_modules.cpp.
Previously CMake was not aware of which headers files the generation
of `gparams_register_modules.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declared module description/parameters change.
* New headers are added that declare module description/parameters.
* `.pyg` files that generate header files that declare module
  description/parameters change

Now the `z3_add_component()` CMake function has been modifed so that

* All header files that are generated from `.pyg` files are added as
dependencies and are scanned from module description/parameter
declarations. This implicit dependency of `gparams_register_modules.cpp`
depending on other generated header files seems unnecessary complex. We
should revisit this design decision once the Python/Makefile build
system is deprecated.

* The function now takes an optional `EXTRA_REGISTER_MODULE_HEADERS`
argument which allows the headers that declare module
description/paramters to be explicitly listed.

With this information CMake will now regenerate `gparams_register_modules.cpp`
correctly.

This required the `mk_gparams_register_modules_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
2017-06-21 23:56:46 +01:00
Arie Gurfinkel
372e8b3c49 expose iterator api of obj_hashtable 2017-06-20 21:07:38 -04:00
Arie Gurfinkel
f3019a3de9 api to accumulate stopwatches 2017-06-20 21:07:38 -04:00
Dan Liew
4b517b96df [CMake] Move CMake files into their intended location so the
`contrib/cmake/bootstrap.py` script no longer needs to be executed.

The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.

The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.

This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
2017-06-12 11:59:00 +01:00
Christoph M. Wintersteiger
596652ed36 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-31 18:35:52 +01:00
Christoph M. Wintersteiger
a7d5bb7b36 Tabs 2017-05-31 12:18:00 +01:00
Nikolaj Bjorner
23ff580a67 get rid of timeb dependencies, pull request #1040
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-23 12:16:43 -07:00
Nikolaj Bjorner
2834fea9b3 fix x64 warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-23 08:58:21 -07:00
Lev Nachmanson
1b62592015 change in a comment
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2017-05-18 13:44:00 -07:00
Nikolaj Bjorner
79a8e9aab0 fix build break #1029
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-18 12:09:51 -07:00
Nikolaj Bjorner
4069e76ab0 remove unused column function field, #1021
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-16 21:27:43 -07:00
Nikolaj Bjorner
3290a933b5 remove spurious include file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-14 14:09:42 -07:00
Nikolaj Bjorner
a0efdc21c3 add missing locks around mpz operations that access object allocator. Use internal skolem constant for theory assumption to hide it from models
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-14 14:04:00 -07:00
Lev Nachmanson
07f2fd43bb Merge remote-tracking branch 'upstream/master' 2017-05-11 17:49:33 -07:00
Lev Nachmanson
d0d71a0907 allow more failures in d_solver
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2017-05-11 17:49:27 -07:00
Nikolaj Bjorner
a9e2a1204e add this qualifier for build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 16:58:29 -07:00
Nikolaj Bjorner
7b35eacf63 add this qualifier for build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 16:52:54 -07:00
Nikolaj Bjorner
2ab0f281f3 add this qualifier for build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 16:50:39 -07:00
Nikolaj Bjorner
29a49f4427 convert static random fields to non-static
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 16:46:07 -07:00
Lev Nachmanson
cf8b35a6f3 fix init reorder warning
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
2017-05-11 10:54:18 -07:00
Nikolaj Bjorner
431feab1bf fix build warnings part 8
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 09:37:01 -07:00
Nikolaj Bjorner
7e004fe331 fix build warnings part 7, disable LRA for regression t201.smt2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 09:28:59 -07:00
Nikolaj Bjorner
49d2b86d35 fix build warnings part 6
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 08:57:17 -07:00
Nikolaj Bjorner
b9a695633d fix build issues part 4 2017-05-11 08:18:20 -07:00
Nikolaj Bjorner
6e021781cd fix build issues part 3
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 07:49:41 -07:00
Nikolaj Bjorner
fcfaedd9ec fix build issues part 2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 07:39:56 -07:00
Nikolaj Bjorner
2a905e02c8 fix build issues part 1
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-11 07:38:52 -07:00
Nikolaj Bjorner
714dfaded3 Merge pull request #1017 from levnach/123
123
2017-05-11 07:31:40 -07:00
Lev Nachmanson
b08f094620 merging with the lp fork
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2017-05-10 16:53:25 -07:00
Nikolaj Bjorner
f03f471f02 fix for #1016
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-10 15:13:04 -07:00
Lev Nachmanson
cf695ab876 taking changes from the fork
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2017-05-10 10:43:01 -07:00
Nikolaj Bjorner
74ac58de2b enable generic parameters with smt-tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-10 10:18:50 -07:00
Nikolaj Bjorner
f572c79cdb add instances
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 19:55:24 -07:00
Nikolaj Bjorner
f4544eb060 disambiguating arguments to unordered map erase and dealing with unused and uninitialized variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 15:35:00 -07:00
Nikolaj Bjorner
d43c12413d add disambiguation, avoid uninitialzed variable passing in debug mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 15:27:42 -07:00
Nikolaj Bjorner
f12f83af83 fix warnings, avoid class qualification in static function
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 14:56:38 -07:00
Nikolaj Bjorner
c5f1f8ba59 missing files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-05-09 14:14:58 -07:00