3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 01:54:08 +00:00
Commit graph

9889 commits

Author SHA1 Message Date
Nikolaj Bjorner c802a0ac96 fix crash exposed by examples/dotnet/Program.cs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-20 14:32:59 -07:00
Nikolaj Bjorner 3ba2aa2672 regressions in examples/dotnet/Program.cs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-20 14:01:43 -07:00
Nikolaj Bjorner 8f90176883 fix symbol comparison
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-20 13:54:55 -07:00
Nikolaj Bjorner 39d8053a54 remove dummy contracts
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-20 10:32:09 -07:00
Nikolaj Bjorner 3d37060fa9 remove dependencies on contracts
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-20 10:24:36 -07:00
Nikolaj Bjorner 12fc670839
Merge pull request #1893 from flopp/spelling
Fix some spelling errors (mostly in comments).
2018-10-20 08:51:41 -07:00
Florian Pigorsch 326bf401b9 Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
Christoph M. Wintersteiger 880ce12e2d
Fixed .NET Core API build. 2018-10-20 12:03:47 +01:00
Nikolaj Bjorner 6233dee505 double happiness
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-19 21:05:32 -07:00
Nikolaj Bjorner 7835091a26 good luck!
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-19 21:03:47 -07:00
Nikolaj Bjorner 7cc6d84e6f merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-19 21:02:15 -07:00
Nikolaj Bjorner 694a6a26c9 bump version, add double access
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-19 20:20:08 -07:00
Nikolaj Bjorner 28a5a515a8 fix #1889
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-18 09:20:12 -07:00
Nikolaj Bjorner 566bdf3a82 add self-contained section on where to retrieve binaries
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-17 09:55:15 -07:00
Nikolaj Bjorner bbc1afb3a6 Merge branch 'master' of https://github.com/z3prover/z3 2018-10-17 09:47:49 -07:00
Nikolaj Bjorner a6ad893f54 add instructions as gift for Klaus
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-17 09:47:44 -07:00
Nikolaj Bjorner c8187c900e
Merge pull request #1886 from waywardmonkeys/use-bool-literals-more
Use bool literals instead of 0/1.
2018-10-17 09:45:10 -07:00
Nikolaj Bjorner 9e780bf46e
Merge pull request #1887 from waywardmonkeys/fix-doxygen-warnings
Fix doxygen warnings.
2018-10-17 09:44:19 -07:00
Nikolaj Bjorner de4a59af40
Merge pull request #1888 from waywardmonkeys/fix-typos
Fix some typos.
2018-10-17 09:44:04 -07:00
Bruce Mitchener 372cab2c5b Fix some typos. 2018-10-17 22:49:39 +07:00
Bruce Mitchener f082735af6 Fix doxygen warnings. 2018-10-17 22:47:39 +07:00
Bruce Mitchener dda62ae78c Use bool literals instead of 0/1. 2018-10-17 22:42:57 +07:00
Nikolaj Bjorner 8431a54190
Merge pull request #1878 from 0xCM/master
Fixes git error discussed in  https://github.com/Z3Prover/z3/pull/1552
2018-10-16 17:05:53 -07:00
Nikolaj Bjorner 40ea00be4b
Merge pull request #1884 from janisozaur/const-ret
Remove superfluous const from returned types
2018-10-16 17:05:18 -07:00
Nikolaj Bjorner fe1cf3274d
Merge pull request #1883 from janisozaur/catch-by-ref
Catch exceptions by const-reference
2018-10-16 17:04:50 -07:00
Michał Janiszewski 844f400a62 Remove superfluous const from returned types 2018-10-16 19:30:48 +02:00
Michał Janiszewski cfd0486582 Catch exceptions by const-reference
Exceptions caught by value incur needless cost in C++, most of them can
be caught by const-reference, especially as nearly none are actually
used. This could allow compiler generate a slightly more efficient code.
2018-10-16 19:16:07 +02:00
Nikolaj Bjorner b301a59899
Merge pull request #1881 from Z3Prover/revert-1880-c++17
Revert "Made Z3 compile for C++17 with MSVC"
2018-10-15 12:52:38 -07:00
Nikolaj Bjorner 6704a4be02
Revert "Made Z3 compile for C++17 with MSVC" 2018-10-15 12:52:19 -07:00
Nikolaj Bjorner 4916de874b
Merge pull request #1880 from mjp41/c++17
Made Z3 compile for C++17 with MSVC
2018-10-15 12:52:07 -07:00
Nikolaj Bjorner 016872a5e0 increment patch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-15 12:44:19 -07:00
Nikolaj Bjorner c8d00fb5b4 follow instructions from #1879
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-15 11:44:47 -07:00
Matthew Parkinson 01005a46f6 Made it more legal C++17 2018-10-15 17:25:34 +01:00
Chris Moore a8f26ae1d8 Fixes the git submodule error discussed in https://github.com/Z3Prover/z3/pull/1552 2018-10-15 10:09:41 -05:00
Nikolaj Bjorner b1ab473035 add arguments to optimize_check fix #1866
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-14 20:44:46 -07:00
Nikolaj Bjorner 09e40f6e23 add arguments to optimize_check fix #1866
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-14 20:43:35 -07:00
Nikolaj Bjorner 0457b5a73f add arguments to optimize_check fix #1866
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-14 20:39:54 -07:00
Nikolaj Bjorner 5b51e69137 fix #1874 by removing nnf.skolemize option
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-14 18:17:34 -07:00
Nikolaj Bjorner 70f3fa36c5 remove qualifiers that downlevel compilers complain about
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-13 09:39:48 -07:00
Nikolaj Bjorner 6277ed61c9 pull rounding mode top-level to deal with build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-13 02:09:35 -07:00
Nikolaj Bjorner 5f4da31b19
Merge pull request #1869 from nabice/master
Ignore current dir when searching for jni
2018-10-12 22:45:32 -07:00
Nikolaj Bjorner 973c9602f8 Merge branch 'master' of https://github.com/z3prover/z3 2018-10-12 22:44:33 -07:00
Nikolaj Bjorner 5356c4f7dd remove class from enum class, add default to avoid compiler warning
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-12 22:44:23 -07:00
Nikolaj Bjorner 3a6d735d0a
Merge pull request #1877 from waywardmonkeys/signed_comparison
dl_util: Use an unsigned to match other values.
2018-10-12 22:41:58 -07:00
Bruce Mitchener 58682c20be dl_util: Use an unsigned to match other values. 2018-10-13 07:58:27 +07:00
Nikolaj Bjorner efb12331e0
Merge pull request #1873 from xlauko/master
Add a floating-point support to c++ api.
2018-10-12 10:52:55 -07:00
Nikolaj Bjorner 5d1d3821b9
Merge pull request #1876 from waywardmonkeys/typo-fixes
Typo fixes.
2018-10-12 10:44:33 -07:00
Bruce Mitchener 5bd93b8a77 Typo fixes. 2018-10-12 23:38:53 +07:00
Nikolaj Bjorner a58bc72dfb Merge branch 'master' of https://github.com/z3prover/z3 2018-10-11 22:05:15 -07:00
Nikolaj Bjorner f5fea8ae30 add parameter to force sat-cleaning on initialization and on simplification phases
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-10-11 22:05:04 -07:00