3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 10:51:50 +00:00
Commit graph

15291 commits

Author SHA1 Message Date
Iain Scott c18f012c83
Remove x64 suffix from NuGet package names. (#5292) 2021-05-21 13:51:02 -07:00
Jakob Rath 089015b250
Minor fix in sat::literal (#5293) 2021-05-21 13:50:01 -07:00
Matt Thornton ce1a48486e
Fix NuGet package name and glibc rid. (#5290) 2021-05-21 08:41:29 -07:00
Nikolaj Bjorner 17be37a5f6 fix #5287 2021-05-20 15:40:18 -07:00
Nikolaj Bjorner a59dcfdeab update python tag
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-20 15:23:39 -07:00
Matt Thornton 9cc1549dbe
Use osx-x64 for mac rid rather than macos. (#5288) 2021-05-20 15:19:31 -07:00
Nikolaj Bjorner 03d2c5f3d0 consolidate literals 2021-05-20 12:58:27 -07:00
Nikolaj Bjorner c959e28d4a remove prints, remove ability to toggle eager_eq_axioms option
NB. Spacer sets eager_eq_axioms option to false, but relevancy of this option is not clear at all as all other default paths don't use this option and theory_lra is incorrect when it is set to false.
2021-05-20 04:26:45 -07:00
Nikolaj Bjorner cc12e3ed38 fix #5280 2021-05-19 16:52:24 -07:00
Nikolaj Bjorner e0860ea173 fix #5279 2021-05-19 13:31:31 -07:00
Nikolaj Bjorner ec034679ce #5215
memory leaks
2021-05-19 12:42:38 -07:00
Nikolaj Bjorner abe3ef2382 #5215 2021-05-19 10:33:23 -07:00
Nikolaj Bjorner d450fd4227 #5215 2021-05-19 10:03:49 -07:00
Nikolaj Bjorner 7b3a587505 fix #5225 2021-05-18 18:04:03 -07:00
Nikolaj Bjorner 9031b5b949 fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-18 11:46:46 -07:00
Nikolaj Bjorner 0490056e7a na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-17 19:19:28 -07:00
Nikolaj Bjorner 30974968af fix #5256
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-17 17:41:34 -07:00
Nikolaj Bjorner 4f9ad28a05 fix #5252 2021-05-17 16:16:12 -07:00
Nikolaj Bjorner 55f8ad068f fix #5262 2021-05-17 15:51:03 -07:00
Nikolaj Bjorner 8384f38eb5 fix #5254 2021-05-17 15:42:01 -07:00
Nikolaj Bjorner 1a432529dd fix #5272 2021-05-17 11:10:05 -07:00
Nikolaj Bjorner d2bd92eab9 fix #5271 2021-05-17 10:42:34 -07:00
Nikolaj Bjorner 93a9847815 BUILD_LIBZ3_SHARED
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-16 15:44:44 -07:00
Margus Veanes 8ca6f567d3
fixing issue #5140 (#5268) 2021-05-16 13:53:08 -07:00
Zachary Wimer f942c3df91
operator= checks this equality before moving (#5265) 2021-05-12 13:10:14 -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 cd82205b06 nit 2021-05-10 19:14:18 -07:00
Nikolaj Bjorner d27d09f87a #5261 2021-05-10 13:35:25 -07:00
Nikolaj Bjorner 897a2d6470 #5261 2021-05-10 13:33:37 -07:00
Nikolaj Bjorner f02fbb49bb fix #5253 2021-05-10 13:00:52 -07:00
Nikolaj Bjorner 2ea4b0f4e0 #5260 2021-05-10 11:42:11 -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 28328e63fd fix #5255
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-09 20:48:11 -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
Philipp Schröer 7373946d67
julia: fix duplicate method (#5251)
Resulted in "Double registration for method" errors when loading Z3.jl
with a current build of Z3.
2021-05-07 14:00:33 -07:00
Nikolaj Bjorner 7e7360dd0c #5223 2021-05-05 17:40:42 -07:00
Nikolaj Bjorner 7e330c15e7 #5223 2021-05-05 16:57:06 -07:00
Nikolaj Bjorner 87c0a8136f #5223 2021-05-05 16:11:21 -07:00
Nikolaj Bjorner 2b1b10be69 fix #5236 2021-05-05 13:50:53 -07:00
Nikolaj Bjorner 85bd4b5242 #5223
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-05 13:10:53 -07:00
Lev Nachmanson 179988e161
support recursive terms (#5246)
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2021-05-05 12:53:20 -07:00
Murphy Berzish 466269ee13
theory_str iterator refactoring and dead code removal (#5222)
* z3str3: iterator refactoring

* z3str3: remove old nfa dead code

* z3str3: continued iterator refactoring

* z3str3: remove unroll dead code

* z3str3: ctx_dep_analysis iterator refactoring

* z3str3: continued iterator refactoring

* z3str3: final iterator refactoring
2021-05-05 10:06:03 -05:00
Nikolaj Bjorner 0c6722f48b na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-03 11:47:00 -07:00
Nikolaj Bjorner 60cf482cea fix #5239
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-03 11:44:44 -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 ff480d1183 fix #5238 2021-05-02 16:09:01 -07:00
Nikolaj Bjorner 51a4db862a #5223 2021-05-02 10:40:22 -07:00
Nikolaj Bjorner 0810720267 #5223 2021-05-02 10:30:35 -07:00