summaryrefslogtreecommitdiff
path: root/src/smt/command.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/command.h')
-rw-r--r--src/smt/command.h5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/smt/command.h b/src/smt/command.h
index b823b5730..41776cee5 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -46,7 +46,10 @@ class Term;
class SmtEngine;
class Command;
class CommandStatus;
+
+namespace smt {
class Model;
+}
std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
@@ -995,7 +998,7 @@ class CVC4_PUBLIC GetModelCommand : public Command
OutputLanguage language = language::output::LANG_AUTO) const override;
protected:
- Model* d_result;
+ smt::Model* d_result;
}; /* class GetModelCommand */
/** The command to block models. */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback