mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
12750 commits 23 branches 48 tags 157 MiB
Commit graph

1820 commits

Author SHA1 Message Date
Nikolaj Bjorner 41ab578593 remove assert, remove brittle pydoc example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-17 00:35:47 -10:00
Nikolaj Bjorner 234b53b831 fix #3028 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-17 00:20:01 -10:00
Nikolaj Bjorner 8428970a1f fix #3006 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-16 23:46:58 -10:00
Nikolaj Bjorner 8c35b2092d fix #3022 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-16 08:14:51 -10:00
Nikolaj Bjorner e9c4c23334 fix #3017 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-15 21:42:22 -10:00
Nikolaj Bjorner 17984af4cc disable automatic coersion to reals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-11 22:06:04 -08:00
Nikolaj Bjorner 67cc2a8cf0 fix #2939 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-05 04:51:35 -08:00
Nikolaj Bjorner 28c827fb69 fix #2919 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-02 14:49:35 -08:00
Nikolaj Bjorner b0a28160f7 fix #2921 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-02 10:35:06 -08:00
Nikolaj Bjorner 3dc822c127 fix #2903 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 18:48:27 -08:00
Nikolaj Bjorner be95ea121b fix #2912 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 17:32:19 -08:00
Nikolaj Bjorner 321329d77c fix #2910 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 14:31:13 -08:00
Nuno Lopes d79692b185 remove unused file & hide a few symbols 2020-01-31 17:13:28 +00:00
Lev ef87054fe0 take ast.cpp from Z3Prover master 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 09f5ae7521 add a clear() method to nla_solver, fix a bug in abs values tables, add assertions, fix newtral lemma generation 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev d301a9c403 rebase with z3prover 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Nikolaj Bjorner d913a55dfb reset m_explanation (#82) 
* reset m_explanation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* streamline handling of m_explanation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-28 10:04:21 -08:00
Nikolaj Bjorner ee62f83131 fix #2892 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-27 20:59:02 -08:00
Nikolaj Bjorner ca11dc1fc5 remove ad-hoc rewriting of division related to comparison. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-27 17:36:02 -08:00
comet eea7805551 update 2020-01-27 15:27:11 -08:00
Nikolaj Bjorner 9c0e350bc4 rewrite3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-26 18:50:58 -08:00
Nikolaj Bjorner c8c088e80d fix #2891 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-26 17:50:00 -08:00
Nikolaj Bjorner 5497022f5c fix #2877 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-24 17:56:23 -06:00
Nikolaj Bjorner ce0ccc2e9e fix #2860 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-24 16:33:57 -06:00
Nikolaj Bjorner d3b105f9f8 move out sign 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-20 16:22:38 -06:00
Nikolaj Bjorner 89c91765f6 fix 2863 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-20 16:22:37 -06:00
Nikolaj Bjorner ab5905cf7f some adjustments for stack use on large strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-12 22:08:24 -08:00
Nikolaj Bjorner e2f5c1f7c8 delay load specrels 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:18:56 -08:00
Nikolaj Bjorner 541658fe02 move to abstract symbols 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:14:13 -08:00
Nikolaj Bjorner 78a1736bd2 prepare symbols to be more abstract, update mbi, delay initialize some modules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:02:08 -08:00
Nikolaj Bjorner f70696d8e7 reduce contention #2842 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-06 20:10:11 -08:00
Nikolaj Bjorner 88fc4c82aa use-before-def 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-06 16:41:13 -08:00
Nikolaj Bjorner 2999d33ede reuse m_bv_sym based on stack in #2842 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-06 16:03:45 -08:00
Nikolaj Bjorner ebc9b7fb4e fix #2841 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-06 11:05:00 -08:00
Nikolaj Bjorner a7dc50362b fix #2836 2019-12-31 11:55:43 -08:00
Nikolaj Bjorner 62ea86d5d2 fix #2832 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-29 10:55:58 -08:00
Nikolaj Bjorner ce4e71fbe9 fix #2831 again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-28 18:44:33 -08:00
Nikolaj Bjorner 36b2e7f0fc revert fix for #2821 as it breaks other functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-27 21:38:52 -08:00
Nikolaj Bjorner dd07d21f6c fix #2821 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-27 12:16:28 -08:00
Nikolaj Bjorner 1d77e3e19f fix #2830 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-26 14:41:09 -08:00
Nikolaj Bjorner 5d3a4ee805 fix #2824 fix #2825 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-25 21:06:26 -08:00
Nikolaj Bjorner efbcdcbffd simplify diff rewriting 2019-12-20 23:20:19 -08:00
Nikolaj Bjorner 4389ed0f58 fix #2812 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-20 17:12:44 -08:00
Nikolaj Bjorner 081001971d fix #2794 2019-12-10 01:45:46 -08:00
Nikolaj Bjorner ebb7d60c75 fix #2792 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-09 07:50:57 +03:00
Nikolaj Bjorner 99a91ee116 fix #2793 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-09 07:38:47 +03:00
Nikolaj Bjorner e6dc557c68 fix #2791 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-08 11:09:02 +03:00
Nikolaj Bjorner 7e415c1b69 update to logging 2019-12-04 23:08:41 +03:00
Nikolaj Bjorner 1eab774b91 fix #2774 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-02 15:22:03 -08:00
Nikolaj Bjorner 489448b869 fix #2762, fix #2750, add iterative unrolling to help on termination on sat instances (to address non-termination in #2759 and #2762) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-30 18:05:24 -08:00