diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2012-12-01 00:37:22 +0000 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2012-12-01 00:37:22 +0000 |
| commit | e39b94aa9425123420635c298fa6bb8a2ee4f048 (patch) | |
| tree | 13f5a5a0b0e1588c632c69678cf60e448abd438d /examples/api/bitvectors.cpp | |
| parent | 8298c65be9b707775fb1a43ce657c6bc6dd93533 (diff) | |
added a new example for the combination of bit-vectors and arrays (includes model generation) and set the logic for the bitvector example
Diffstat (limited to 'examples/api/bitvectors.cpp')
| -rw-r--r-- | examples/api/bitvectors.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index 364fdb69e..4701bf8e3 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -26,7 +26,8 @@ int main() { ExprManager em; SmtEngine smt(&em); smt.setOption("incremental", true); // Enable incremental solving - + smt.setLogic("QF_BV"); // Set the logic + // The following example has been adapted from the book A Hacker's Delight by // Henry S. Warren. // |