mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-05 20:35:41 +00:00
Code Activity
7821 commits 40 branches 51 tags 168 MiB
Commit graph

277 commits

Author SHA1 Message Date
Nikolaj Bjorner
b78c538e02 fix build of test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-30 22:58:41 -08:00
Nikolaj Bjorner
c31ad14747 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 00:52:32 -08:00
Nikolaj Bjorner
4bb0e9b633 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 00:52:06 -08:00
Nikolaj Bjorner
89971e2a98 remove smtlib1 dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 10:37:30 -08:00
Nikolaj Bjorner
d67f3c1466 create proofs folder, move proof-post-order utility to proofs directory, fix regression with proofs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 03:08:56 -07:00
Nikolaj Bjorner
72c9134424 fixing regressions introduced when reducing astm proof dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 02:26:39 -07:00
Christoph M. Wintersteiger
01f642a6f3 Backward compatibility 2017-10-16 18:19:55 +01:00
Nuno Lopes
912a729097 fix build of unit tests 2017-10-16 00:54:30 +01:00
Nikolaj Bjorner
7f8a7c3d83 fix the fixme of #1307 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-14 11:59:09 -07:00
Nikolaj Bjorner
6ecd77d91c Merge branch 'master' of https://github.com/z3prover/z3 2017-10-12 14:17:57 -07:00
Nikolaj Bjorner
3554554533 command to exit tests early 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 14:17:52 -07:00
Nikolaj Bjorner
d338fab4f6 fix #1305 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 13:58:14 -07:00
Nikolaj Bjorner
11f1a81d7b disable failing unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 10:12:37 -07:00
Nikolaj Bjorner
6a09040a8e Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-12 07:39:38 -07:00
Nikolaj Bjorner
da2b876acb fix #1303 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 07:39:27 -07:00
Dan Liew
a3b109cc14 [ASan] Fix some leaks reported in the small object allocator 
test.
 2017-10-11 19:40:16 +01:00
Nikolaj Bjorner
bec60f763b add diagnostics to DDNF and fix #1268 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-30 12:35:36 -07:00
Nikolaj Bjorner
2751cbc270 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-23 22:36:36 -05:00
Christoph M. Wintersteiger
6d51265d9d Cleaned up LP test code. 2017-09-17 17:14:30 +01:00
Christoph M. Wintersteiger
00651f8f21 Tabs, formatting. 2017-09-17 14:54:09 +01:00
Nikolaj Bjorner
9f5bd2feda fix front-end for datatype 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-05 19:58:05 -07:00
Nikolaj Bjorner
06087c17be support for legacy datatype test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-05 10:28:11 -07:00
Nikolaj Bjorner
f12a4f04fd aligning simplifier and rewriter for regression tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-04 09:28:40 -07:00
Nikolaj Bjorner
a3dba5b2f9 hide new datatype plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-03 20:01:59 -07:00
Nikolaj Bjorner
d940516df3 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-27 11:01:45 -07:00
Nikolaj Bjorner
bcf229dcfd removing dependencies on simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-26 11:23:41 -07:00
Nikolaj Bjorner
ee00852151 fix compilation of tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-17 21:09:23 -07:00
Nikolaj Bjorner
4d07fa5db3 use ifdef instead of if for _TRACE 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 12:46:38 -07:00
Nikolaj Bjorner
be8add44e9 instrument unit test to use reproducible random number generator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 12:42:08 -07:00
Christoph M. Wintersteiger
81a7f37acc Fixed LP tests 2017-08-01 18:33:47 +01:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 13:24:11 -07:00
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
a0a8bc2a62 fixes to #1155 and partial introduction of SMTLIB 2.6 datatype format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-24 09:12:43 -07:00
Nikolaj Bjorner
cba9a160d3 deal with warning messages 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 19:42:22 -07:00
Nikolaj Bjorner
bd92797663 fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 15:25:59 -07:00
Nikolaj Bjorner
a1306eaab6 fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 13:17:37 -07:00
Nikolaj Bjorner
253870c6d7 fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 13:08:23 -07: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
Nikolaj Bjorner
3f89c1418b fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 12:51:14 -07:00
Nikolaj Bjorner
64f3b3e316 remove lp_main from test branch to ensure test build only builds a single entry point 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-12 07:59:16 -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
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
2a905e02c8 fix build issues part 1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-11 07:38:52 -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
c5f1f8ba59 missing files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-09 14:14:58 -07:00
Nikolaj Bjorner
911b24784a merge LRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-09 10:46:11 -07:00
Murphy Berzish
41a242fab1 Merge branch 'upstream-master' into develop 
Conflicts:
	src/smt/params/smt_params.h
	src/smt/params/smt_params_helper.pyg
	src/smt/smt_case_split_queue.cpp
	src/smt/smt_context.h
	src/smt/smt_setup.cpp
	src/smt/smt_setup.h
 2017-05-03 17:03:13 -04:00
Nikolaj Bjorner
eeb79e1c3c update to retain original behavior 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 19:30:54 -07:00
Nikolaj Bjorner
561a4331a8 add back use of all variables for tracking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 16:36:05 -07:00