diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-30 10:53:52 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-30 10:53:52 -0400 |
| commit | fa53ae111cd314f455456a884f1247bb9b8e2c7b (patch) | |
| tree | 2eb9d36e5e20d2160c7d49b6f89f162b54a20d64 /examples/api | |
| parent | f4d031742d969c689d38c0756a5026a434ef89b3 (diff) | |
Use FS as the set-logic string for theory of sets
Diffstat (limited to 'examples/api')
| -rw-r--r-- | examples/api/sets.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp index 79168e06a..7390eefe0 100644 --- a/examples/api/sets.cpp +++ b/examples/api/sets.cpp @@ -26,6 +26,10 @@ int main() { ExprManager em; SmtEngine smt(&em); + // Optionally, set the logic. We need at least UF for equality predicate, + // integers (LIA) and sets (FS). + smt.setLogic("QF_UFLIAFS"); + // Produce models smt.setOption("produce-models", true); |