mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-20 14:20:31 +00:00
Code Activity
5750 commits 41 branches 52 tags 175 MiB
Commit graph

4703 commits

Author SHA1 Message Date
Nikolaj Bjorner
746d26e744 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-29 21:14:52 -08:00
Nikolaj Bjorner
e63724a22d replace assert by SASSERT in case of unsupported proof rule 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-29 15:30:42 -08:00
Nikolaj Bjorner
bd9b5b5735 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-29 10:13:19 -08:00
Christoph M. Wintersteiger
2f08040403 typo 2015-12-29 16:00:07 +00:00
Christoph M. Wintersteiger
b0781a14cd Fix for FP numeral construction in the Python API. Fixes #386. 2015-12-29 15:59:14 +00:00
Nikolaj Bjorner
e2fab0a555 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-28 18:15:48 -08:00
Nikolaj Bjorner
739043e273 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-28 10:28:43 -08:00
Nikolaj Bjorner
071a654a9a seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-27 04:41:25 -08:00
Nikolaj Bjorner
31302ec851 automata 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-25 15:22:26 -08:00
Nikolaj Bjorner
4a5b645d88 automata 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-25 05:37:24 -08:00
Nikolaj Bjorner
659a7ede84 automata 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-25 04:25:23 -08:00
Nikolaj Bjorner
65d147106e automata 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-24 12:01:59 -08:00
Nikolaj Bjorner
1bbf7813b0 automata 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-24 03:30:02 -08:00
Nikolaj Bjorner
2a7f2ab7f8 sequence automaton 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-23 20:33:55 -08:00
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
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
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
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
ed1e8b73ed formatting 2015-12-17 17:39:23 +00:00
Mikolas Janota
0fd61eee1f Cleanup in lackr. 2015-12-17 13:25:56 +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
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
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
c33a8794a4 Merge branch 'master' of https://github.com/Z3Prover/z3 into new_ocaml_install 2015-12-14 16:32:48 +00:00
Christoph M. Wintersteiger
e652b7d2c7 Follow-up fix for #377. 2015-12-14 16:31:10 +00:00
Christoph M. Wintersteiger
4f5a2e432d For for Python 3.x __eq__/__hash__. 
Fixes #377.
 2015-12-14 16:27:39 +00:00
Christoph M. Wintersteiger
ced6809cd8 Removed old, unnecessary file. 2015-12-14 14:43:28 +00:00
Christoph M. Wintersteiger
134b93b43e ML API build fixes for Windows. 2015-12-14 14:41:19 +00:00
Christoph M. Wintersteiger
1f0b5cd0bc Merge branch 'master' of https://github.com/Z3Prover/z3 into new_ocaml_install 2015-12-14 13:02:49 +00:00