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

8928 commits

Author SHA1 Message Date
Nikolaj Bjorner 0520d1a1f6 remove trial with mfsr flag
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-08 07:38:30 -07:00
Nikolaj Bjorner 24adae4166 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-07 22:03:16 -07:00
Nikolaj Bjorner 4547f2c001 enable non-expression bodies of quantifiers to fix #1667
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-07 22:03:03 -07:00
Nikolaj Bjorner 29c2672407 fix bugs exposed by Nuno's PB example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-07 21:43:37 -07:00
Nuno Lopes 9e916edcb0 z3.py: add overflow checks to PB API 2018-06-07 15:40:04 +01:00
Nikolaj Bjorner 88ead235f0 gcc mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-06 19:30:56 -07:00
Nikolaj Bjorner bb53060313 int64_t
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-06 19:26:40 -07:00
Nikolaj Bjorner 8565de2c5b deal with shift exponent error
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-06 19:17:37 -07:00
Nikolaj Bjorner ad67424987 deal with shift exponent error
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-06 18:23:04 -07:00
Nikolaj Bjorner d7f51f2443 try flags to fix gcc build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-06 18:20:23 -07:00
Nikolaj Bjorner 99bdb46158 int64_t
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-06 17:48:30 -07:00
Nikolaj Bjorner 8ab428b660 try new gcd
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-06 17:42:44 -07:00
Nikolaj Bjorner add8d26807 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-01 08:07:14 -07:00
Nikolaj Bjorner fee4f91e2d add set operations to python request by Francois
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-01 08:07:06 -07:00
Nikolaj Bjorner e2eb883c71 Merge branch 'master' of https://github.com/z3prover/z3 2018-05-30 16:48:17 -07:00
Nikolaj Bjorner b9637924c4 fix #1662
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-30 16:47:17 -07:00
Nikolaj Bjorner 0d668e1428 fix #1661
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-30 03:18:22 -07:00
Nikolaj Bjorner 0aa3245c37 Merge branch 'master' of https://github.com/z3prover/z3 2018-05-29 20:55:46 -07:00
Nikolaj Bjorner db3f439e88 fix memory leak from Arie
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-29 20:55:30 -07:00
Nikolaj Bjorner 6dc9c3a587 fix ml build breakd #1659, #1660
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-29 07:37:27 -07:00
Nikolaj Bjorner da0239d200 fix #1655
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-25 21:21:27 -07:00
Nikolaj Bjorner 727ba13566 fix #1653
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-25 12:55:04 -07:00
Nikolaj Bjorner a06926915d remove stale file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-25 10:47:54 -07:00
Nikolaj Bjorner b37a5b1679 clean up python build files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-25 10:27:12 -07:00
Nikolaj Bjorner 434ff31629
Merge pull request #1646 from NikolajBjorner/master
Remove depedencies on interp
2018-05-25 10:25:31 -07:00
Nikolaj Bjorner d66f2af45e Merge branch 'master' of https://github.com/z3prover/z3 2018-05-25 08:56:40 -07:00
Nikolaj Bjorner 753b9dd734 fix #1650 fix #1648
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-25 08:56:13 -07:00
Nikolaj Bjorner af2fecd724
Merge pull request #1651 from Z3Prover/revert-1650-add-soname-to-libz3.so
Revert "Fix missing SONAME in libz3.so, which breaks loading from Java"
2018-05-25 08:43:56 -07:00
Nikolaj Bjorner 2b73b7c7f3
Revert "Fix missing SONAME in libz3.so, which breaks loading from Java" 2018-05-25 08:43:35 -07:00
Nikolaj Bjorner 19fb3e98dc
Merge pull request #1650 from PhilippWendler/add-soname-to-libz3.so
Fix missing SONAME in libz3.so, which breaks loading from Java
2018-05-25 07:44:32 -07:00
Nikolaj Bjorner 7145a9ac41 fix #1647
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-25 07:38:30 -07:00
Nikolaj Bjorner 8eeaa27cf3 remove interp from documentation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-25 07:33:43 -07:00
Philipp Wendler 3e0506a71b Set the SONAME field of libz3.so to libz3.so.
This fixes a problem when loading libz3java from Java,
where the dependency on libz3 is not detected as fulfilled
if the latter does not have SONAME set.
2018-05-25 15:01:07 +02:00
Nikolaj Bjorner 6b700f1f5f remove interpolation from test_capi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-24 20:32:04 -07:00
Nikolaj Bjorner 9f3da32a77 remove interpolation from test_capi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-24 16:28:23 -07:00
Nikolaj Bjorner a9ca01d8d3 deprecating interp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-24 13:12:07 -07:00
Nikolaj Bjorner da32997f93 fix #1638
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-24 10:15:36 -07:00
Nikolaj Bjorner 6ecae2b986 fix #1645
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-24 09:21:20 -07:00
Nikolaj Bjorner 4f5775c531 remove interpolation and duality dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-24 08:33:48 -07:00
Nikolaj Bjorner d088a1b9f6 updated release notes for merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-23 18:25:14 -07:00
Nikolaj Bjorner 2e4fb8d356 work around VS2012 compiler bug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-23 16:33:27 -07:00
Nikolaj Bjorner 278fd03f19 GLU -> GNU fix #1643
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-23 13:31:55 -07:00
Nikolaj Bjorner a9b1966ff2 Merge branch 'master' of https://github.com/z3prover/z3 2018-05-23 10:30:22 -07:00
Nikolaj Bjorner f9bdfe2978 fix x86 warning
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-23 10:30:14 -07:00
Nikolaj Bjorner b1e83dfc58
Merge pull request #1642 from waywardmonkeys/cxx-docs-missing-word
Fix missing word in C++ API docs.
2018-05-23 10:01:29 -07:00
Nikolaj Bjorner 148ccc93f0
Merge pull request #1641 from waywardmonkeys/remove-proof-mode-from-ocaml-docs
Update OCaml docs for changes made elsewhere.
2018-05-23 10:01:11 -07:00
Nikolaj Bjorner 77aef356cf
Merge pull request #1640 from waywardmonkeys/z3-true-false-bool
Z3_TRUE/Z3_FALSE should be true/false, not 1/0.
2018-05-23 10:00:48 -07:00
Bruce Mitchener 6db90a9333 Fix missing word in C++ API docs. 2018-05-23 23:58:08 +07:00
Bruce Mitchener a3facc82fb Update OCaml docs for changes made elsewhere.
This removes references to the PROOF_MODE that have been removed
elsewhere.
2018-05-23 23:55:17 +07:00
Bruce Mitchener 510cb5ee6e Z3_TRUE/Z3_FALSE should be true/false, not 1/0.
Now that Z3_bool is a C bool, the associated constants should
be as well.
2018-05-23 23:51:36 +07:00