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

216 commits

Author SHA1 Message Date
Nikolaj Bjorner
f810f25d8d fix #3004
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-02-17 19:37:47 -10:00
Nikolaj Bjorner
b71595f5b1 fix #3003
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-02-14 17:51:31 -10:00
Nikolaj Bjorner
541658fe02 move to abstract symbols
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-01-10 12:14:13 -08:00
Nikolaj Bjorner
cdf3c48349 clear memory on allocation to avoid msan warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-29 15:50:49 -08:00
Nikolaj Bjorner
6cf7d8e523 adding div0
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-06 11:23:19 +01:00
Christoph M. Wintersteiger
efa3c0f68e
Fix compiler warnings 2019-10-28 14:15:25 +00:00
Nikolaj Bjorner
7bfb730fee fix traffic jam
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-10 17:45:55 -07:00
Nuno Lopes
2f33bafd5a stopwatches: fix a few places that would call start/stop multiple times 2019-02-21 14:59:31 +00:00
Bruce Mitchener
5fa861fa95 Simplify some boolean returns. 2018-12-04 22:41:31 +07:00
Bruce Mitchener
2016f48dc9 Avoid const params in decls.
Const-qualification of parameters only has an effect in function
definitions.
2018-11-28 19:07:33 +07:00
Bruce Mitchener
e570940662 Prefer using empty rather than size comparisons. 2018-11-27 21:42:04 +07:00
Bruce Mitchener
1082fad27a Fix typos. 2018-11-11 22:21:43 +07:00
Florian Pigorsch
326bf401b9 Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
Nikolaj Bjorner
797e576195 unreferenced variable in release mode, spaces
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-29 21:25:08 -07:00
Nikolaj Bjorner
06c9a9f3e1 merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-27 08:51:22 -07:00
Nikolaj Bjorner
5762be2a0f fix 1703
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-27 08:49:52 -07:00
Nikolaj Bjorner
520ce9a5ee integrate lambda expressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-26 07:23:04 -07:00
Nikolaj Bjorner
6fc08e9c9f Merge branch 'master' of https://github.com/z3prover/z3 2018-06-15 14:58:10 -07:00
Nikolaj Bjorner
a51d6cbcbc debug model evaluator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-15 14:58:02 -07:00
Nikolaj Bjorner
ff0f257102 remove iff
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:48 -07:00
Nikolaj Bjorner
e94b97376c fix memory leak in relation_manager, use for loops
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 10:16:03 -07:00
Bruce Mitchener
2fa304d8de Remove int64, uint64 typedefs in favor of int64_t / uint64_t. 2018-03-31 14:45:04 +07:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Bruce Mitchener
7167fda1dc Use override rather than virtual. 2018-02-10 09:56:33 +07: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
Bruce Mitchener
ae8027e594 Fix typos. 2018-02-01 19:39:43 +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
Bruce Mitchener
73b3da37d8 Typo fixes. 2018-01-02 22:48:06 +07:00
Nuno Lopes
9b54b4e784 fix vector<> to support non-POD types
adjust code to std::move and avoid unnecessary/illegal
2017-10-16 00:54:29 +01:00
Nikolaj Bjorner
06d75a616f fix #1288, again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-08 11:40:17 +01:00
Nikolaj Bjorner
22fa108ffd fix #1288, again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-08 11:07:22 +01:00
Nikolaj Bjorner
a5ecf87ab8 fix #1288
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-08 10:32:38 +01:00
Nikolaj Bjorner
eac659f748 deal with empty set of post-orders
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-06 11:34:14 +01:00
Christoph M. Wintersteiger
00651f8f21 Tabs, formatting. 2017-09-17 14:54:09 +01:00
Nikolaj Bjorner
cf87b6d622 remove simplifier files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-29 09:22:27 -07:00
Nikolaj Bjorner
ce04c18a7a trying to get rid of last simplifier dependency in macros
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-22 22:14:13 -07:00
Nikolaj Bjorner
66b24a6c18 change typename to class in optional to deal with compilation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-08-17 21:00:14 -07:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 13:24:11 -07:00
Nikolaj Bjorner
253870c6d7 fix compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-04 13:08:23 -07:00
Nikolaj Bjorner
08524a2d90 cleanup for warning message
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-01 11:47:17 -07:00
Arie Gurfinkel
c7fbab0c11 propagate rule names during xform 2017-06-23 09:38:04 -04:00
Dan Liew
4b517b96df [CMake] Move CMake files into their intended location so the
`contrib/cmake/bootstrap.py` script no longer needs to be executed.

The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.

The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.

This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
2017-06-12 11:59:00 +01:00
Nikolaj Bjorner
aff02ca905 include 'stopwatch.h' to avoid ODR warnings, #994 2017-04-30 11:28:11 -07:00
Nikolaj Bjorner
c1480b4389 handle model generation from issue #748. Deal with warnings from #836
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-12-12 00:40:52 +01:00
Nikolaj Bjorner
0765eea486 add suggestions from #835
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-12-11 05:45:40 +01:00
Nikolaj Bjorner
32c63ce4cd address other warnings per input from delcypher
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-12-10 17:23:59 +01:00
Nikolaj Bjorner
6594c3a046 add virtual destructor to intermediary class in case this helps for #835
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-12-10 13:58:39 +01:00
Nikolaj Bjorner
dea3b8ddf7 address warnings from #836
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-12-10 13:14:36 +01:00
Nikolaj Bjorner
8e078cf9e2 address #835
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-12-10 07:52:00 +01:00