Tuples and records merge. Resolves bug 270.

Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.

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

1 files changed, 8 insertions, 2 deletions

diff --git a/src/util/util_model.cpp b/src/util/util_model.cpp
index bb2924b51..0c058fce9 100644
--- a/src/util/util_model.cpp
+++ b/src/util/util_model.cpp
@@ -36,11 +36,17 @@ Model::Model() :
 }
 
 size_t Model::getNumCommands() const {
-  return d_smt.d_modelCommands->size();
+  return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size();
 }
 
 const Command* Model::getCommand(size_t i) const {
-  return (*d_smt.d_modelCommands)[i];
+  Assert(i < getNumCommands());
+  // index the global commands first, then the locals
+  if(i < d_smt.d_modelGlobalCommands.size()) {
+    return d_smt.d_modelGlobalCommands[i];
+  } else {
+    return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()];
+  }
 }
 
 }/* CVC4 namespace */