mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
6986 commits 49 branches 53 tags 182 MiB
Commit graph

6986 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
f414869456 add symbolic automaton 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-23 19:46:10 -08:00
Nikolaj Bjorner
386399472d seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-23 11:02:34 -08:00
Christoph M. Wintersteiger
077e801590 Assertion fix. Relates to #383. 2015-12-23 13:41:52 +01:00
Nikolaj Bjorner
7a9bd72e2e merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-22 17:48:47 -08:00
Nikolaj Bjorner
72d2cd546e elim_bounds bugfix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-22 17:48:02 -08:00
Nikolaj Bjorner
0b1e8ff912 removing tabs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-22 17:00:00 -08:00
Nikolaj Bjorner
5262e1986c removing tabs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-22 16:58:26 -08:00
Christoph M. Wintersteiger
ced4a430d1 ML code simplification 2015-12-22 23:40:27 +00:00
Christoph M. Wintersteiger
0f656047c7 ML code simplification 2015-12-22 23:37:07 +00:00
Christoph M. Wintersteiger
d6b7645d11 Merge pull request #385 from tigertoes/master 
Fixing building under OS X
 2015-12-22 23:48:22 +01:00
Nikolaj Bjorner
54e8612f4d fix bounds elimination bug for nested quantifiers. Codeplex post z3: A formula and its negation are unsatisfiable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-22 12:26:38 -08:00
Nikolaj Bjorner
4cf41c44f3 support else values that are null from models 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-22 11:09:48 -08:00
Nikolaj Bjorner
ea876715e3 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-22 10:46:50 -08:00
Nikolaj Bjorner
995d66c6f2 remove print statements 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-22 10:46:33 -08:00
Nikolaj Bjorner
9c6271dded add debugging facilities for github issues #384 #367 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-22 10:43:18 -08:00
Tony Tiger
e98ee6ec06 Fixing building under OS X 
Previous method is_osx_hack didn't exist, possibly wasn't cleaned up. This
change has been tested and Z3 compiles successfully within a 2.7 virtualenv
running on OS X 10.10.5.
 2015-12-22 13:00:55 +00:00
Christoph M. Wintersteiger
a30fe1e2ec Followup to previous build fix. Relates to #357 and #361 2015-12-22 00:52:37 +01:00
Christoph M. Wintersteiger
ea218da2c4 Bugfix in build scripts. 
Additional fix for #357, relates to #361.
 2015-12-22 00:37:27 +01:00
Nikolaj Bjorner
65da0f9f3a updated seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-21 06:07:50 -08:00
Nikolaj Bjorner
8e26c97782 tuning bit-vector operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-21 13:09:03 +02:00
Nikolaj Bjorner
1eebab355c Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-20 09:44:16 +02:00
Nikolaj Bjorner
284fcc2c04 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-20 09:43:56 +02:00
Christoph M. Wintersteiger
c2ab9b72dc resource-limit related fixes in src/test 2015-12-18 18:43:38 +00:00
Christoph M. Wintersteiger
e91b1e1da4 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-17 17:39:27 +00:00
Christoph M. Wintersteiger
ed1e8b73ed formatting 2015-12-17 17:39:23 +00:00
Mikolas Janota
0fd61eee1f Cleanup in lackr. 2015-12-17 13:25:56 +00:00
Christoph M. Wintersteiger
06deb07a49 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-17 12:47:34 +00:00
Christoph M. Wintersteiger
0fe1e3248f .NET build fix 2015-12-17 12:47:24 +00:00
Christoph M. Wintersteiger
1cc2385fd2 typo 2015-12-17 12:33:45 +00:00
Mikolas Janota
3dbc307ecd Setting up the lackr branch. 2015-12-16 20:10:14 +00:00
Mikolas Janota
4cc1640a45 Adding stats to lackr. 2015-12-16 14:41:54 +00:00
Nikolaj Bjorner
99da56a786 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-16 00:49:36 +02:00
Nikolaj Bjorner
ee0dbf34f0 add completion (introducing negative root function symbols) to address regression introduced when fixing unsound handling of negative roots 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-16 00:49:06 +02:00
Mikolas Janota
c6e66ebc3a Adding ackr component. 2015-12-15 18:43:36 +00:00
Nuno Lopes
dbc1a84d6a fix warning with MSVC++ 64 2015-12-15 18:36:01 +00:00
Christoph M. Wintersteiger
90b1b07af4 build fixes 2015-12-15 15:03:53 +00:00
Christoph M. Wintersteiger
22a77721ef Updated build options for .NET API 2015-12-15 14:20:31 +00:00
Christoph M. Wintersteiger
f4e3989766 .NET API build fixes 2015-12-15 13:09:02 +00:00
Christoph M. Wintersteiger
0da8160716 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-15 12:25:09 +00:00
Christoph M. Wintersteiger
942b6ba5ec Updated .NET build. 2015-12-15 12:24:59 +00:00
Christoph M. Wintersteiger
2fde24b3ab Merge pull request #380 from delcypher/c_api_example_typo 
Typo in comment in C api example.
 2015-12-15 12:03:11 +00:00
Dan Liew
83e2b1c6e5 Typo in comment in C api example. 2015-12-15 11:52:35 +00:00
Christoph M. Wintersteiger
fc5b9156cf Merge pull request #363 from delcypher/dotnet_configure_assembly_info 
Refactor ``mk_all_assembly_infos()`` to use the ``configure_file()`` and misc fixes for dotnet bindings
 2015-12-15 11:35:14 +00:00
Dan Liew
439d8d8afe Fix issue on non-windows systems when emitting the build rule 
for the ".NET" bindings example.

Previously there was a hack that would to path separator replacement
( '/' -> '\' ) which breaks paths under non-windows platforms. The hack
has been made slightly better by doing ( '/' -> os.path.sep). This
preserves the existing behaviour under Windows and unbreaks the build
on non-windows platforms.

I'm not entirely sure why the path replacement needs to be done in
the first place. I thought Windows was supposed to support using
'/' as a path separator (as well as '/'). Maybe ``csc.exe`` doesn't
support these kind of paths?
 2015-12-15 08:56:47 +00:00
Dan Liew
44393b37de Emit dependency of phony target `examples on _ex_dotnet_example` 
when building of the ".NET" bindings is enabled.
 2015-12-15 08:46:47 +00:00
Nikolaj Bjorner
b1459f4fa3 fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-15 04:57:32 +02:00
Nikolaj Bjorner
82c3233967 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-15 04:11:22 +02:00
Nikolaj Bjorner
43bc6caa55 fix warning messages 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-15 04:11:11 +02:00
Christoph M. Wintersteiger
aa7ce540e8 Merge pull request #379 from wintersteiger/new_ocaml_install 
New ocaml install
 2015-12-14 16:45:36 +00:00
Christoph M. Wintersteiger
c33a8794a4 Merge branch 'master' of https://github.com/Z3Prover/z3 into new_ocaml_install 2015-12-14 16:32:48 +00:00