Nikolaj Bjorner
|
e96f9de70b
|
perf #1988
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-29 06:02:32 -08:00 |
|
Nikolaj Bjorner
|
8248ec879e
|
fix qsat destructor memory allocation #1948
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-28 15:35:46 -08:00 |
|
Nikolaj Bjorner
|
45dd820b6c
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2018-11-28 13:50:40 -08:00 |
|
Nikolaj Bjorner
|
5dc1337476
|
fix #1984 - already fixed in private branch, but wasn't propagated to master
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-28 13:49:53 -08:00 |
|
Nikolaj Bjorner
|
3fe9b76fe5
|
Merge pull request #1986 from mtrberzi/issue1908
Z3str3: correct str.replace semantics
|
2018-11-28 13:15:39 -08:00 |
|
Murphy Berzish
|
e76e501216
|
Z3str3: correct str.replace semantics
|
2018-11-28 14:42:19 -05:00 |
|
Nikolaj Bjorner
|
f2de15a665
|
Merge pull request #1982 from waywardmonkeys/avoid-const-params-in-decls
Avoid const params in decls.
|
2018-11-28 09:08:03 -08:00 |
|
Nikolaj Bjorner
|
ee5ae8fb5e
|
Merge pull request #1983 from waywardmonkeys/missing-ref
mk_coeffs_without was inadvertently copying src.
|
2018-11-28 09:07:15 -08:00 |
|
Nikolaj Bjorner
|
a78380901e
|
Merge pull request #1976 from waywardmonkeys/use-nullptr-more
Use nullptr rather than 0/NULL.
|
2018-11-28 09:06:40 -08:00 |
|
Nikolaj Bjorner
|
649eb53ef9
|
Merge pull request #1977 from waywardmonkeys/fix-typos
Fix a couple of typos.
|
2018-11-28 09:04:35 -08:00 |
|
Bruce Mitchener
|
a3281a02db
|
mk_coeffs_without was inadvertently copying src.
Pass it via ref.
|
2018-11-28 20:12:47 +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
|
090f14e7bc
|
Fix a couple of typos.
|
2018-11-28 14:58:04 +07:00 |
|
Bruce Mitchener
|
b83d6d77c9
|
Use nullptr rather than 0/NULL.
|
2018-11-28 14:57:01 +07:00 |
|
Nikolaj Bjorner
|
eea9b79035
|
Merge pull request #1975 from Bronsa/null_wrapped
Guard against null wrapped functions in OCaml API
|
2018-11-27 10:44:20 -08:00 |
|
Nikolaj Bjorner
|
c5f280ae6e
|
Merge pull request #1969 from Bronsa/master
Catch and print exceptions in Z3_mk_config
|
2018-11-27 10:43:43 -08:00 |
|
Nikolaj Bjorner
|
5df29daa35
|
Merge pull request #1972 from waywardmonkeys/use-vector-empty
Prefer using empty rather than size comparisons.
|
2018-11-27 10:39:34 -08:00 |
|
Nikolaj Bjorner
|
7b68d3d893
|
Merge pull request #1973 from waywardmonkeys/modernize-use-override
Use 'override' in new code.
|
2018-11-27 10:37:35 -08:00 |
|
Nikolaj Bjorner
|
4bbf90c57f
|
Merge pull request #1974 from waywardmonkeys/fix-ocaml-typo
Fix typo in OCaml API docs.
|
2018-11-27 10:37:24 -08:00 |
|
Nikolaj Bjorner
|
2b34e4f738
|
fix #1968
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-27 10:36:03 -08:00 |
|
Nicola Mometto
|
ad49c3269a
|
Guard against null wrapped functions in OCaml API
|
2018-11-27 18:11:29 +00:00 |
|
Bruce Mitchener
|
7fb0106ead
|
Fix typo in OCaml API docs.
|
2018-11-27 22:14:41 +07:00 |
|
Bruce Mitchener
|
64ac929301
|
Use 'override' in new code.
|
2018-11-27 22:07:14 +07:00 |
|
Bruce Mitchener
|
e570940662
|
Prefer using empty rather than size comparisons.
|
2018-11-27 21:42:04 +07:00 |
|
Nicola Mometto
|
21158d87e3
|
override n_mk_config in ml bindings to catch exception path
|
2018-11-27 12:31:00 +00:00 |
|
Nicola Mometto
|
29a28f544d
|
catch and print exceptions in Z3_mk_config instead of letting them
bubble up the stack
|
2018-11-27 12:31:00 +00:00 |
|
Nikolaj Bjorner
|
253f457425
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2018-11-26 21:13:10 -08:00 |
|
Nikolaj Bjorner
|
503bedbc7a
|
fix #1967:
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-26 21:12:47 -08:00 |
|
Nikolaj Bjorner
|
4686429318
|
Merge pull request #1967 from Bronsa/master
Add Memory.reset to OCaml API
|
2018-11-26 20:33:00 -08:00 |
|
Nicola Mometto
|
f18227bf2d
|
Add Memory.reset to OCaml API
|
2018-11-26 17:24:51 +00:00 |
|
Nikolaj Bjorner
|
a83097d5cc
|
Merge pull request #1964 from waywardmonkeys/remove-define-void
Remove unused DEFINE_VOID macro.
|
2018-11-26 08:09:36 -08:00 |
|
Bruce Mitchener
|
b2123136b1
|
Remove unused DEFINE_VOID macro.
|
2018-11-26 09:20:04 +07:00 |
|
Nikolaj Bjorner
|
e026f96ed4
|
code review updates for #1963
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-25 14:30:30 -08:00 |
|
Nikolaj Bjorner
|
abfb9989b6
|
Merge pull request #1963 from Nils-Becker/master
Logging Improvements for the Axiom Profiler
|
2018-11-25 14:25:35 -08:00 |
|
Nikolaj Bjorner
|
8e83d04e02
|
this->size()
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-25 14:22:22 -08:00 |
|
Nikolaj Bjorner
|
88fd088a09
|
conditional flattening
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-25 14:15:10 -08:00 |
|
Nikolaj Bjorner
|
16be5b0e7d
|
fix #1816 - m_parent_selects gets updated while accessing an interator, fix is to rely on the size of the vector for iteration
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-25 14:04:17 -08:00 |
|
nilsbecker
|
b57a483a6c
|
using obj_hashtable instead of unordered_set as suggested by Nikolaj
|
2018-11-25 22:50:14 +01:00 |
|
nilsbecker
|
165b256d32
|
ensure equalities between terms bound to quantified variables are always logged
|
2018-11-25 20:34:25 +01:00 |
|
nilsbecker
|
1e4f524a22
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2018-11-25 16:58:09 +01:00 |
|
Nikolaj Bjorner
|
aa723f1eee
|
fix uninitialized variable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-24 18:13:35 -08:00 |
|
Nikolaj Bjorner
|
074ed0d874
|
fix warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-24 17:39:19 -08:00 |
|
Nikolaj Bjorner
|
32df9b1155
|
mac build errors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-24 17:34:53 -08:00 |
|
Nikolaj Bjorner
|
96043216e5
|
fix unsound unfolding
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-24 17:25:56 -08:00 |
|
Nikolaj Bjorner
|
6ddbc9cd38
|
overhaul of regular expression membership solving. Use iterative deepening and propagation, coallesce intersections
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-24 15:26:39 -08:00 |
|
Nikolaj Bjorner
|
d61d9d4ce3
|
remove reject states
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-24 11:06:51 -08:00 |
|
Nikolaj Bjorner
|
33eb82c25a
|
remove prefix2prefix, fix #1566
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-23 23:36:47 -08:00 |
|
Nikolaj Bjorner
|
069949a576
|
fix model construction for semantics of itos
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-23 22:30:13 -08:00 |
|
Nikolaj Bjorner
|
20a28af225
|
fix stoi/itos axiom replay
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-23 21:42:48 -08:00 |
|
Nikolaj Bjorner
|
d55af41955
|
constrain lengths
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-11-23 19:54:34 -08:00 |
|