3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Commit graph

10255 commits

Author SHA1 Message Date
Nikolaj Bjorner 02f01fcef1 adding esrp feature
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-11 17:31:09 -08:00
Nikolaj Bjorner 93c59ffbd9 update script to sign assembly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-11 15:48:33 -08:00
Nikolaj Bjorner c1b03e8ca6 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-11 09:38:44 -08:00
Nikolaj Bjorner bfcea7a819 perf improvements by reordering variable branching #1676
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-11 09:38:36 -08:00
Nikolaj Bjorner 271e86020a Merge branch 'master' of https://github.com/z3prover/z3 2018-12-11 09:35:34 -08:00
Nikolaj Bjorner 045fef35ed fix build break
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-11 09:35:27 -08:00
Nikolaj Bjorner 021c5315a7
Merge pull request #2034 from Bronsa/patch-1
Change error message from "internal failure" to "Object allocation failed"
2018-12-11 09:32:32 -08:00
Nikolaj Bjorner a3f9e3168d simplify ~context #1948
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-11 09:29:59 -08:00
Nikolaj Bjorner 796689f708 #1948 remove memory allocation in nlsat::solver::~solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-11 09:08:53 -08:00
Nicola Mometto 06fc94818f
Change error message from "internal failure" to "Object allocation failed"
For consistency with ad49c3269a and Java/dotNet APIs
2018-12-11 12:09:22 +00:00
Nikolaj Bjorner da5486563d Merge branch 'master' of https://github.com/z3prover/z3 2018-12-10 18:38:15 -08:00
Nikolaj Bjorner 092c25d596 fix #2007
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-10 18:37:30 -08:00
Nikolaj Bjorner b40c2b2926 fix #876
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-10 14:11:00 -08:00
Nikolaj Bjorner 68ace83893 remove enable trace
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-10 07:34:56 -08:00
Nikolaj Bjorner f2a7bcaf5d remove prints
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-09 14:38:45 -08:00
Nikolaj Bjorner bb69aa88fb Merge branch 'master' of https://github.com/z3prover/z3 2018-12-09 12:56:26 -08:00
Nikolaj Bjorner 604e5dd0bb fixing #2030
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-09 12:56:21 -08:00
Nikolaj Bjorner 45bf7887e4
Merge pull request #2032 from waywardmonkeys/enable-dl-table-tests
Enable dl_table tests on non-Windows/Cygwin.
2018-12-09 20:01:21 +01:00
Bruce Mitchener 1b91694d9b Enable dl_table tests on non-Windows/Cygwin. 2018-12-09 21:02:06 +07:00
Nikolaj Bjorner 559f57470e fix #2031
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-09 08:21:48 +01:00
Nikolaj Bjorner 2ca83d0095 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-08 15:42:13 +01:00
Nikolaj Bjorner 38b5e6de56 fix #2019 - insufficient axioms for special cases
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-08 13:57:35 +01:00
Nikolaj Bjorner f1d1e728ff
Merge pull request #2021 from waywardmonkeys/api-bool-reduction
Simplify boolean code.
2018-12-07 18:59:45 +00:00
Nikolaj Bjorner a20e68facc throttel extract/ite rewriting to avoid perf-bug exposed in example from Lucas Cordeiro and Alessandro Trindade
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-07 17:54:49 +00:00
Bruce Mitchener 0231bc44bc Simplify boolean code.
Now that the C API is using bool, this can be simplified.
2018-12-07 22:06:51 +07:00
Nikolaj Bjorner a9946685ca
Merge pull request #2024 from UniQP/caseLabels
Fix enum type of case labels
2018-12-06 07:43:01 -08:00
Nikolaj Bjorner e1b1953ff1
Merge pull request #2025 from msoeken/nuget-release
Changes to NuGet release script
2018-12-06 07:41:52 -08:00
Mathias Soeken 9a0a1dd818 Changes to NuGet release script. 2018-12-06 16:19:03 +01:00
Sebastian Buchwald 5690dbcbfd Fix enum type of case labels 2018-12-06 00:08:29 +01:00
Nikolaj Bjorner f2c263001c
Merge pull request #2020 from waywardmonkeys/fix-typos
Fix typos.
2018-12-05 13:16:23 -08:00
Bruce Mitchener 4bc1b0b8c8 Fix typos. 2018-12-05 21:07:34 +07:00
Nikolaj Bjorner 9635ddd8fc fix #2018
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-05 00:54:10 -08:00
Nikolaj Bjorner dc77579707 delta faction to control double lookahead eagerness
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-04 23:41:03 -08:00
Nikolaj Bjorner 44b2c3ce6b
Merge pull request #2016 from Z3Prover/revert-2015-c++-api-use-nullptr
Revert "Use nullptr, not 0 in the C++ API impl."
2018-12-04 12:07:10 -08:00
Nikolaj Bjorner 3b54575340
Revert "Use nullptr, not 0 in the C++ API impl." 2018-12-04 12:06:44 -08:00
Nikolaj Bjorner 0223846b4f
Merge pull request #2015 from waywardmonkeys/c++-api-use-nullptr
Use nullptr, not 0 in the C++ API impl.
2018-12-04 10:18:23 -08:00
Nikolaj Bjorner 7aaacbfc62
Merge pull request #2014 from waywardmonkeys/simplify-boolean-returns
Simplify some boolean returns.
2018-12-04 10:17:53 -08:00
Nikolaj Bjorner 4b94ea112d
Merge pull request #2013 from waywardmonkeys/remove-get-manager
Remove Z3_get_manager.
2018-12-04 10:17:29 -08:00
Nikolaj Bjorner 3551d12168
Merge pull request #2011 from waywardmonkeys/missing-Z3_API
Z3_fixedpoint_add_constraint: decl missing Z3_API.
2018-12-04 10:17:12 -08:00
Nikolaj Bjorner 2372d1bdeb
Merge pull request #2012 from waywardmonkeys/doc-fixups
Fix up more documentation formatting.
2018-12-04 10:16:27 -08:00
Nikolaj Bjorner a6d8818be4 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-04 10:14:42 -08:00
Nikolaj Bjorner 9e5aaf074e perf improvements for #1979
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-04 10:13:55 -08:00
Bruce Mitchener 924776eaa6 Use nullptr, not 0 in the C++ API impl. 2018-12-04 22:43:01 +07:00
Bruce Mitchener 5fa861fa95 Simplify some boolean returns. 2018-12-04 22:41:31 +07:00
Bruce Mitchener 374b80f37f Remove Z3_get_manager.
This was publicly exported from the shared library, but it isn't
in any header files and isn't used anywhere in the repository.
2018-12-04 21:38:33 +07:00
Bruce Mitchener 15e1a5ee86 Fix up more documentation formatting. 2018-12-04 20:20:21 +07:00
Bruce Mitchener 6c21d3d9e8 Z3_fixedpoint_add_constraint: decl missing Z3_API. 2018-12-04 12:24:42 +07:00
Nikolaj Bjorner e15a39f463
Merge pull request #2010 from waywardmonkeys/doc-markup-z3-l-consts
Mark up Z3_L_TRUE and friends correctly in the docs.
2018-12-03 19:01:05 -08:00
Bruce Mitchener 42d2a46826 Mark up Z3_L_TRUE and friends correctly in the docs. 2018-12-04 09:12:12 +07:00
Nikolaj Bjorner ea0d253308 fix const-char test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-03 11:56:20 -08:00