diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e7bb8795c..c154db399 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1216,6 +1216,13 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) parseError( "eqrange predicate requires option --arrays-exp to be enabled."); } + if (kind == api::SINGLETON && args.size() == 1) + { + api::Sort sort = args[0].getSort(); + api::Term ret = d_solver->mkSingleton(sort, args[0]); + Debug("parser") << "applyParseOp: return singleton " << ret << std::endl; + return ret; + } api::Term ret = d_solver->mkTerm(kind, args); Debug("parser") << "applyParseOp: return default builtin " << ret << std::endl; |