mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity
14406 commits 23 branches 48 tags 157 MiB
Commit graph

204 commits

Author SHA1 Message Date
Nikolaj Bjorner c0a07f9229 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-14 04:26:59 -07:00
Nikolaj Bjorner c4a03dcf7c remove temporary comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-14 04:13:30 -07:00
Nikolaj Bjorner 9729db16a2 always reduce macro expansions in model evaluation #4588 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-13 17:39:15 -07:00
Nikolaj Bjorner 094e41d21d build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-13 16:40:41 -07:00
Nikolaj Bjorner 780346c7ca address model generation bugs raised in #4518 and #4324 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-24 13:22:19 -07:00
Nikolaj Bjorner 71a32f5bb2 remove unused 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-22 11:38:27 -07:00
Nuno Lopes 23e6adcad3 fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string 2020-07-11 20:24:45 +01:00
Nikolaj Bjorner d0e20e44ff booyah 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:56:30 -07:00
Nikolaj Bjorner 655166b867 randomize generation of 'some value' for user sorts. #4557 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-01 16:34:09 -07:00
Nikolaj Bjorner 1be22a80f6 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-11 17:20:18 -07:00
Nikolaj Bjorner 884a68251b fix #4266 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-11 16:53:59 -07:00
Nikolaj Bjorner 39fb44fe09 fix #4200 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-03 18:10:54 -07:00
Nikolaj Bjorner 2a93ac3d81 fix #4200 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-03 18:10:26 -07:00
Nikolaj Bjorner a884201d62 remove using insert_if_not_there2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-25 15:08:51 -07:00
Nikolaj Bjorner 9ea1cf3c5c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-25 13:13:25 -07:00
Nikolaj Bjorner ad8eb8fdcb #4024 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-19 22:44:02 -07:00
Arie Gurfinkel 2b27aa1ce6 fix #3908 2020-04-11 13:58:10 -04:00
Nikolaj Bjorner 56358a6b94 fix #3867 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 18:06:37 -07:00
Nikolaj Bjorner 8e6bb30c82 cleanup bit2bool from models #3847 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 03:06:01 -07:00
Nikolaj Bjorner 35f184a6b9 fix #3826 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-07 14:39:54 -07:00
Nikolaj Bjorner 4c69f9e31b invalid model regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 15:27:06 -07:00
Nikolaj Bjorner f0a6837c67 invalid model regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 15:17:09 -07:00
Nikolaj Bjorner ea08fcf65c invalid model regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 15:15:48 -07:00
Nikolaj Bjorner be1109e80f turn on model evaluation for as-array, #2420 #3646 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 12:25:12 -07:00
Nikolaj Bjorner cc394f0fe9 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 03:42:13 -07:00
Nikolaj Bjorner c142f99127 fix #3532 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 11:00:02 -07:00
Nikolaj Bjorner 0a97f37be5 fix #3284 (and other recent regressions) 2020-03-12 08:37:43 -07:00
Nikolaj Bjorner bdd66e1fa0 fix #3180 fix #3181 #3184 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-07 12:13:43 +01:00
Nikolaj Bjorner 153d0661fe fix #3141 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-05 07:57:21 +01:00
Nikolaj Bjorner 2882a6708e fix #2957 - arrays are treated as values 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 16:35:13 -08:00
Nikolaj Bjorner 8428970a1f fix #3006 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-16 23:46:58 -10:00
Nikolaj Bjorner 806ee85759 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-11 14:25:25 -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 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 1e0c1cefd6 add definitions for under-specified cases of arithmetic operators #2663 #2676 #2679 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-06 18:24:22 +01:00
Nikolaj Bjorner 6cf7d8e523 adding div0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-06 11:23:19 +01:00
Christoph M. Wintersteiger 2308d8af09
Fix for partially interpreted floating-point functions. Relates to #2596, #2631. 2019-10-28 14:15:29 +00:00
Nikolaj Bjorner 203ba12abc moving to context reset model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-18 19:22:46 -07:00
Nikolaj Bjorner 4ce6b53d95 fix #2640 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-16 20:40:03 -07:00
Nikolaj Bjorner ca498e20d1 move value factories to model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-16 19:48:35 -07:00
Nikolaj Bjorner 39edf73e78 fix #2613 fix #2612 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-05 16:57:51 -07:00
Nikolaj Bjorner feff1f7f96 fix #2609 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-02 14:40:11 -07:00
Nikolaj Bjorner a635049e23 fill in ad-hoc interpretation for division by 0. #2561 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-01 20:07:31 -07:00
Nikolaj Bjorner 000e485794 add array selects to basic ackerman reduction improves performance significantly for #2525 as it now uses the SAT solver core instead of SMT core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-01 12:17:19 -07:00
Nikolaj Bjorner 4c0db00a7b fix push/pop bug for ite-elimination, thanks to Nao Hirokawa for reporting it 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-30 08:31:37 -03:00
Nikolaj Bjorner a8bfab3273 add model.inline_def option to make #2517 happy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-29 12:08:09 -03:00
Nikolaj Bjorner 809b0ebca7 revert fix to #2417 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-24 11:24:01 -07:00
Nikolaj Bjorner e65a5d0f47 fix #2420 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-24 09:56:11 -07:00
Daniel Schemmel 5e5c231712
Remove unused variables 2019-07-23 11:09:50 +02:00