3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Commit graph

7880 commits

Author SHA1 Message Date
Christoph M. Wintersteiger 0ef33a98c4
Revert "Fix encoding error" 2018-02-13 14:08:55 +00:00
Nikolaj Bjorner eab7ae58be fix #1484
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-12 23:30:10 -08:00
Nikolaj Bjorner 792fdb915f remove deprecated comments about bv2int/int2bv being treated as uninterpreted, raise in #1481
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-12 13:07:09 -08:00
Nikolaj Bjorner e1100af52c ensure that final model is logged by the time it is produced fix #1463
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-12 12:04:24 -08:00
Nikolaj Bjorner 29ab1ab64b
Merge pull request #1483 from waywardmonkeys/modernize-use-nullptr
Use nullptr.
2018-02-12 11:15:20 -08:00
Bruce Mitchener 76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Nikolaj Bjorner f01328c65f
Merge pull request #1482 from waywardmonkeys/modernize-use-override-2
Use override rather than virtual.
2018-02-11 21:36:07 -08:00
Bruce Mitchener 7167fda1dc Use override rather than virtual. 2018-02-10 09:56:33 +07:00
Nikolaj Bjorner ce123d9dbc
Merge pull request #1480 from waywardmonkeys/modernize-use-override
Use override rather than virtual.
2018-02-09 09:16:58 -08:00
Bruce Mitchener b7d1753843 Use override rather than virtual. 2018-02-09 21:19:27 +07:00
Nikolaj Bjorner 2b847478a2
Merge pull request #1478 from waywardmonkeys/unnecessary-value-param-fixes
Remove unnecessary value parameter copies.
2018-02-09 02:20:47 -08:00
Nikolaj Bjorner d3a98aee94
Merge pull request #1479 from waywardmonkeys/fix-more-typos
Fix typos.
2018-02-09 02:18:45 -08:00
Bruce Mitchener 757b7c66ef Remove unnecessary value parameter copies. 2018-02-09 16:35:34 +07:00
Bruce Mitchener 50f3e9c3c0 Fix typos. 2018-02-09 16:35:26 +07:00
Nikolaj Bjorner 3f7453f5c5 fixing build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-07 20:23:31 -08:00
Nikolaj Bjorner 61934d8106 align semantics of re.allchar with string proposal. #1475
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-07 20:08:15 -08:00
Nikolaj Bjorner 1ee7871bbf to fix #1476
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-06 18:48:03 -08:00
Nikolaj Bjorner cb6896087d fix #1468
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-06 10:21:02 -08:00
Nikolaj Bjorner 159e6ad987
Merge pull request #1472 from levnach/dev
adding template definitions
2018-02-06 07:52:16 -08:00
Lev Nachmanson c74ad46682 remove a duplicate definition
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2018-02-05 21:22:46 -08:00
Nikolaj Bjorner 309012e127
Merge pull request #1474 from waywardmonkeys/inconsistent-missing-override
Fix inconsistent missing override warnings.
2018-02-05 20:33:56 -08:00
Nikolaj Bjorner 755a1b8c1f
Merge pull request #1473 from waywardmonkeys/vector-reserve
Reserve vector space when possible.
2018-02-05 20:32:02 -08:00
Bruce Mitchener 5911f810ed Fix inconsistent missing override warnings. 2018-02-06 11:23:08 +07:00
Bruce Mitchener 54b3cd0071 Reserve vector space when possible.
This fixes all current instances of the
`performance-inefficient-vector-operation`
warning in clang-tidy.
2018-02-06 11:21:17 +07:00
Nikolaj Bjorner b2bd4dd3b4 fix #1471
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-05 18:54:14 -08:00
Nikolaj Bjorner b8680f8a46 Merge branch 'master' of https://github.com/z3prover/z3 2018-02-05 18:33:39 -08:00
Nikolaj Bjorner a1d4e485a4 fix #1469
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-05 18:33:31 -08:00
Nikolaj Bjorner 9d37257059
Merge pull request #1465 from waywardmonkeys/fix-typos
thanks
2018-02-05 18:31:09 -08:00
Nikolaj Bjorner 3e810d6c54 remove static from format (not thread safe), remove std::move #1466
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-05 16:46:49 -08:00
Nikolaj Bjorner 2853558bc2
Merge pull request #1466 from waywardmonkeys/reduce-copying
Use const refs to reduce copying.
2018-02-05 16:37:44 -08:00
Lev Nachmanson a5caa50606 adding template definitions
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2018-02-05 09:42:56 -08:00
Nikolaj Bjorner e332652989 Merge branch 'master' of https://github.com/z3prover/z3 2018-02-04 20:54:49 -08:00
Nikolaj Bjorner 885dfad237 fix #1458
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-04 20:54:21 -08:00
Nikolaj Bjorner 87f7853b9b
Merge pull request #1462 from Firobe/patch-1
Fix encoding error
2018-02-04 16:14:21 -08:00
Christoph M. Wintersteiger 175273fe27 Merge branch 'master' of https://github.com/Z3Prover/z3 2018-02-04 22:43:43 +00:00
Nikolaj Bjorner caaaa23438 Merge branch 'master' of https://github.com/z3prover/z3 2018-02-04 13:06:54 -08:00
Nikolaj Bjorner bf04c38a63 add logging for #1470
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-04 13:06:14 -08:00
Nikolaj Bjorner 20d6543538 set uninitialized fields. Maybe related to #1468
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-04 12:56:21 -08:00
Christoph M. Wintersteiger 333374229d Fixed UFs for unspecified cases of FP conversion operators. Thanks for Youcheng Sun for reporting this bug. 2018-02-03 16:48:05 +00:00
Christoph M. Wintersteiger c3ed986031 Fixed RNA FP rounding mode semantics. Fixes #1190 and bugs reported by Youcheng Sun. 2018-02-03 16:46:21 +00:00
Christoph M. Wintersteiger 8689921e9c Fixed missing bit of precision in fp.to_ubv/fp.to_sbv. Thanks to Youcheng Sun for reporting this bug. 2018-02-03 15:16:23 +00:00
Christoph M. Wintersteiger ad3b0ecad0 Fixed pattern rewriting to produce only valid patterns (which led to a segfault). Bug reported by Youcheng Sun. 2018-02-02 19:27:36 +00:00
Bruce Mitchener ae8027e594 Fix typos. 2018-02-01 19:39:43 +07:00
Nikolaj Bjorner 54ba25175c
Merge pull request #1467 from waywardmonkeys/use-char-rfind
Use char version of rfind.
2018-01-30 08:41:23 -08:00
Bruce Mitchener 6d6b614924 Use char version of rfind.
There is only a single character involved, so use the char version.

This was found via `clang-tidy`.
2018-01-30 21:45:12 +07:00
Bruce Mitchener 177414c0ee Use const refs to reduce copying.
These are things that have been found by `clang-tidy`.
2018-01-30 21:43:56 +07:00
Nikolaj Bjorner 73e9d351dc adding initial model to updated #1463
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-01-30 03:21:58 -08:00
Nikolaj Bjorner 5a16d3ef7f fix license in sstream
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-01-29 19:14:17 -08:00
Nikolaj Bjorner 2f6c80ef08 fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-01-28 12:06:14 -08:00
Nikolaj Bjorner 3e191d5cc5 Merge branch 'master' of https://github.com/z3prover/z3 2018-01-28 11:46:02 -08:00