diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-08-23 16:01:13 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-05 15:17:37 -0400 |
| commit | b3a4670710d3ffdc99879a1d27f37cf775af18eb (patch) | |
| tree | afb6554dcf95cdd324384478a51e01c5d63c106b /src/smt/smt_engine.h | |
| parent | c2972fc63ca6d49ffeaf0e8a9a39cad733790cd7 (diff) | |
Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a segfault in smt2 printer
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 552f5cd67..9f00fad6b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -331,7 +331,7 @@ class CVC4_PUBLIC SmtEngine { * Add to Model command. This is used for recording a command * that should be reported during a get-model call. */ - void addToModelCommandAndDump(const Command& c, bool isGlobal = false, bool userVisible = true, const char* dumpTag = "declarations"); + void addToModelCommandAndDump(const Command& c, uint32_t flags = ExprManager::VAR_FLAG_NONE, bool userVisible = true, const char* dumpTag = "declarations"); /** * Get the model (only if immediately preceded by a SAT |