Bug fix:

* Fix creation of bound variables in CVC native language parser
* This corrects a problem with misleading model output

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 10 insertions, 0 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 57589ec9c..721dedc70 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -179,6 +179,16 @@ Parser::mkVars(const std::vector<std::string> names,
   return vars;
 }
 
+std::vector<Expr>
+Parser::mkBoundVars(const std::vector<std::string> names,
+                    const Type& type) {
+  std::vector<Expr> vars;
+  for(unsigned i = 0; i < names.size(); ++i) {
+    vars.push_back(mkBoundVar(names[i], type));
+  }
+  return vars;
+}
+
 void
 Parser::defineVar(const std::string& name, const Expr& val,
                   bool levelZero) {