mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
15337 commits 24 branches 48 tags 158 MiB
Commit graph

2397 commits

Author SHA1 Message Date
Nikolaj Bjorner
fb75dac63f #5223 2021-05-31 12:01:33 -07:00
Nikolaj Bjorner
50cf321171 fix #5320 2021-05-31 10:18:27 -07:00
Nikolaj Bjorner
83e2e7200c fix #5316 2021-05-30 11:28:31 -07:00
Nikolaj Bjorner
b1606487f0 fix #5289 2021-05-30 10:32:30 -07:00
Nuno Lopes
5a66dfad2a change parameter::hash so that the least significant bits arent overriden 
the 3rd bit was being stuck by the parameter kind, leading to increased number of hash collisions
 2021-05-27 09:38:21 +01:00
Nuno Lopes
36ca98cbbe ast: remove 2 default constructors 2021-05-24 14:59:03 +01:00
Nikolaj Bjorner
2ebab021f2 fix #5297 2021-05-23 13:42:15 -07:00
Nikolaj Bjorner
8919fa4970 #5296 2021-05-23 10:32:09 -07:00
Nuno Lopes
f1e0d5dc8a remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
Nuno Lopes
f8406623b4 switch parameter to an std::variant 
plus fix mem leak & move constructor for zstrings
 2021-05-23 13:07:29 +01:00
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