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

2387 commits

Author SHA1 Message Date
Nikolaj Bjorner fd0778c3d0 fixing symbol -> zstring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-22 14:22:55 -07:00
Nikolaj Bjorner 262daf5151 symbol/zstring transition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-22 13:54:21 -07:00
Nikolaj Bjorner 20a67e47ca remove symbol -> zstring -> symbol round-trips 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-22 13:12:49 -07:00
Nikolaj Bjorner e14e3ef291 #5140 2021-05-22 10:27:53 -07:00
Nikolaj Bjorner e0860ea173 fix #5279 2021-05-19 13:31:31 -07:00
Margus Veanes 8ca6f567d3
fixing issue #5140 (#5268) 2021-05-16 13:53:08 -07:00
Nikolaj Bjorner 7869cdbbc8 #5259 - the Ranjit 2s shave 
shave a couple of seconds from the Ranjit regression
 2021-05-12 10:43:16 -07:00
Nikolaj Bjorner e2a52ed6ee #5259 again 2021-05-10 11:15:19 -07:00
Nikolaj Bjorner 987099c765 Hoist creation of m_rep for #5259 2021-05-10 10:54:21 -07:00
Nikolaj Bjorner a61e9d6b49 #5260 2021-05-10 10:33:43 -07:00
Nikolaj Bjorner 31a5bd7fd7 regression from July 4 2020 tweeted by Dr. RJ and crowd profiled - let's submit this somwhere? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-09 20:33:43 -07:00
Nikolaj Bjorner 7e7360dd0c #5223 2021-05-05 17:40:42 -07:00
Nikolaj Bjorner 2c97799564 #5237 
be stingier on stack instead of punting and saying users can set ulimit
 2021-05-02 16:18:55 -07:00
Nikolaj Bjorner 51a4db862a #5223 2021-05-02 10:40:22 -07:00
Nikolaj Bjorner 323e0e6270 #5223 2021-05-01 16:43:54 -07:00
Nikolaj Bjorner c50e6bdbb1 fix #5229 2021-04-30 02:32:16 -07:00
Nikolaj Bjorner decbf4be11 fix undo record for lblset 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-29 14:06:18 -07:00
Nikolaj Bjorner 308f399224 #5215 converting NYI 2021-04-27 16:19:54 -07:00
Nikolaj Bjorner 22a76e4985 fix typos in comments 2021-04-26 15:15:27 -07:00
Nikolaj Bjorner b1e8303257 #5211 2021-04-24 10:23:09 -07:00
Nikolaj Bjorner 07e2ca100d fix #5213 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-23 10:05:08 -07:00
Nikolaj Bjorner b5496d823d #5211 2021-04-22 23:14:28 -07:00
Nikolaj Bjorner 67ec86fc66 #5211 2021-04-22 22:53:18 -07:00
Nikolaj Bjorner 5d49cb5519 #5211 2021-04-22 22:42:05 -07:00
Nikolaj Bjorner 8263d20e0d add code review comment 2021-04-20 11:30:25 -07:00
Nikolaj Bjorner 4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Nikolaj Bjorner ff1b35663b revert rewriting of OP_LE, OP_GE as it breaks axioms 2021-04-12 09:32:03 -07:00
Nikolaj Bjorner 804f065215 fixes for #4688 
https://github.com/Z3Prover/z3/issues/4866#issuecomment-778721073
 2021-04-11 17:42:12 -07:00
Nikolaj Bjorner f607c15aa2 more rewrites for loop #4373 2021-04-10 11:15:59 -07:00
Nikolaj Bjorner 44156f9f55 patch to fix #5110 2021-04-08 11:25:20 -07:00
Nikolaj Bjorner dcfd9c859d fix build 2021-04-06 21:30:13 -07:00
Nikolaj Bjorner 1b503b8887 na 2021-04-06 20:09:51 -07:00
Nikolaj Bjorner a832ada3d1 fix #5152 2021-04-06 20:09:50 -07:00
Nuno Lopes a6ef99d56e constify ids of builtin AST families + remove some dead code 2021-04-04 18:13:52 +01:00
Nuno Lopes c47ab023e5 remove a few trivial destructors so they get inlined 2021-04-04 17:13:59 +01:00
Nikolaj Bjorner 1fcd537d81 fix #5117 2021-03-30 14:23:30 -07:00
Nikolaj Bjorner c71bbb6391 fix #5136, regression when removing variable registration for mod/div operations 2021-03-30 13:45:54 -07:00
Nikolaj Bjorner 5cc29bec14 simplify ""* to "" 2021-03-29 14:18:57 -07:00
Nikolaj Bjorner 6d28b1a858 fix #5134 2021-03-29 14:11:49 -07:00
Nikolaj Bjorner a352a6638a fix #5126 2021-03-26 14:58:24 -07:00
Nikolaj Bjorner 2fef6dc502 more scaffolding 2021-03-21 11:31:14 -07:00
Nikolaj Bjorner 0b8939d86e self-contained function for merge_tf 2021-03-16 15:24:48 -07:00
Nikolaj Bjorner 9c716a2788 fix #5108 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-16 07:37:06 -07:00
Nikolaj Bjorner 9098084217 reduce overhead of creating seq-plugin, enable parameter cleanup for #5095 2021-03-15 11:54:44 -07:00
Nikolaj Bjorner d62f6c62b5 fix #5096 fix #5099 2021-03-15 09:43:34 -07:00
Nikolaj Bjorner 18143d8932 fix #5102 2021-03-15 01:01:33 -07:00
Nikolaj Bjorner 9a975a4523 array solver fixes 2021-03-13 06:19:32 -08:00
Nikolaj Bjorner f29a596070 deal with compiler warnings, from MacOS CI build 2021-03-08 17:14:09 -08:00
Nikolaj Bjorner 7eceeff349 move branch of unit variable 2021-03-08 10:09:04 -08:00
Nikolaj Bjorner 3c26a965e1 updated script, add comment to mk_eq_empty 2021-03-07 06:59:58 -08:00