3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Commit graph

11553 commits

Author SHA1 Message Date
Nikolaj Bjorner 17fb07875d follow up on #2737
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-25 08:35:28 -08:00
Christoph M. Wintersteiger ba03d99526
Fix forward declaration of fma in C++ API. Fixes #2735. 2019-11-25 11:32:50 +00:00
Nikolaj Bjorner 84025d5c11 add rewrites for moduli as exercised in example from #2319
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-24 19:02:28 -08:00
Nikolaj Bjorner fad4356159 treat division by 0 as non-linearity, fix #2733
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-24 10:52:52 -08:00
Nikolaj Bjorner ca2ad66d03 treat division by 0 as non-linearity
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-24 10:49:35 -08:00
Nikolaj Bjorner e2b6b12215 initialize relvancy level in constructor
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-23 17:26:59 -08:00
Nikolaj Bjorner 5cbabb20ac align readme-cmake and cmakelists.txt according to current state #2732
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-23 15:59:16 -08:00
Nikolaj Bjorner 5dfe4a4b48 ensure relevancy isn't increased between calls
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-23 15:42:44 -08:00
Nikolaj Bjorner 61371b4abf na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-23 15:41:15 -08:00
Murphy Berzish 415260b93d z3str3: refactor app* to app_ref 2019-11-22 16:07:50 -08:00
Nikolaj Bjorner b2c3025e21 fix #2714
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-21 16:37:53 -08:00
Jerry James 8db0429809 Fix "Unbound module Z" error when invoking ocamldoc. 2019-11-21 16:04:17 -08:00
Nikolaj Bjorner e818b8d06f binspr
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-20 16:27:40 -08:00
Nikolaj Bjorner e212159f4e fix #2727
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-20 15:01:10 -08:00
Nikolaj Bjorner a0dcad0221 fix #2708
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-19 21:36:13 -08:00
Nikolaj Bjorner 566eacd424 change handling of weak array mode. Insert weak delay variables into a queue that gets consumed by the next propagation when the array_weak parameter is changed #2686
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-19 21:17:36 -08:00
Nikolaj Bjorner e45bafe9bf increase version number
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-19 14:17:48 -08:00
Nikolaj Bjorner 30e7c225cd upgrade pip
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-19 12:58:44 -08:00
Nikolaj Bjorner f170e655d5 add importlib_metatada
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-19 10:56:56 -08:00
Nikolaj Bjorner c62380ad77 update names of config vars
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-19 08:48:43 -08:00
Nikolaj Bjorner 3669543553 rename additional build options #2709
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 23:06:48 -08:00
Nikolaj Bjorner 429fc7c408 rename additional build options #2709
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 23:02:44 -08:00
Nikolaj Bjorner 2673235dc3 rename additional build options #2709
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 22:55:37 -08:00
Nikolaj Bjorner f7a6f3fa28 fix #2718
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 22:40:33 -08:00
Nikolaj Bjorner c7248a65e4 rename additional build options #2709
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 22:31:45 -08:00
Nikolaj Bjorner dc4adcb147 doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 21:51:28 -08:00
Nikolaj Bjorner 4522e7a97a rename additional build options #2709
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 21:39:11 -08:00
Nikolaj Bjorner 53a01a07bd rename additional build options #2709
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 21:32:35 -08:00
Nikolaj Bjorner 48554f0fb6 rename additional build options #2709
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 21:07:12 -08:00
Nikolaj Bjorner b50f8508f2 rename additional build options #2709
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:50:53 -08:00
Nikolaj Bjorner e9d9792524 rename additional build options #2709
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:39:04 -08:00
Nikolaj Bjorner 3ab9a1c88c remove deprecated USE_OPENMP, rename API_LOG_SYNC to Z3_API_LOG_SYNC (tiny part of #2709)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 20:24:29 -08:00
Nikolaj Bjorner 3729458d14 enable pypi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 19:20:15 -08:00
Nikolaj Bjorner dde8da853e fix bug introduced when fixing #2721
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 13:55:55 -08:00
Nikolaj Bjorner 9b72b60949 block unsound itos solutions. #2721
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 13:44:12 -08:00
Nikolaj Bjorner 29e1fb67d2 fix #2720, unsound preprocessing in elim_uncnstr_tactic where datatype properties of eliminated subterms is forgotten
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 13:34:45 -08:00
Nikolaj Bjorner 05ad90c976 fix for null symbol #2712
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 12:55:24 -08:00
Andrew Helwer 37382d22c4 Updated references to Z3 icon 2019-11-18 12:24:39 -08:00
Andrew Helwer dd4905e377 Publishing SNK file private key for reproducible builds 2019-11-18 12:24:39 -08:00
Nikolaj Bjorner 215edcf888 fix; disable rewrite. fix #2715
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 12:23:03 -08:00
Nikolaj Bjorner fe0b3d6648 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 12:03:59 -08:00
Nikolaj Bjorner 3c6dceae7c fix #2717
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 12:03:59 -08:00
Nikolaj Bjorner d95b549ff8 fix #2707
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-16 17:47:29 -08:00
Nuno Lopes f0b8da42ad typo 2019-11-16 19:27:10 +00:00
Nikolaj Bjorner 2bf595cb8f update release notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-16 10:21:06 -08:00
Nikolaj Bjorner cbac860387 fix #2706
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-16 09:06:58 -08:00
Nuno Lopes b9bc6975e9 fix crash in BV internalizer due to unknown bv_neg symbol 2019-11-16 16:24:24 +00:00
Nikolaj Bjorner cb600a9329 consolidate model.compact and model_compress #2704
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-15 11:07:08 -08:00
Nikolaj Bjorner 1a9dfc5e80 inherit weights
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-14 09:32:55 -08:00
Nikolaj Bjorner 784e2721dd print weight if it is different from default #2667
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-13 19:24:59 -08:00