From 157b5f0d9ce1a7618ce11f7708a72342bf5db55d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 7 May 2013 08:10:43 -0700
Subject: [PATCH] Add expr_vector example

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 examples/c++/example.cpp | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index ab5d0132c..bec8c59a1 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -906,6 +906,28 @@ void enum_sort_example() {
     std::cout << "2: " << result_goal.as_expr() << std::endl;
 }
 
+void expr_vector_example() {
+    context c;
+    const unsigned N = 10;
+
+    expr_vector x(c);
+
+    for (unsigned i = 0; i < N; i++) { 
+        std::stringstream x_name; 
+        x_name << "x_" << i;
+        x.push_back(c.int_const(x_name.str().c_str()));
+    }
+    
+    solver s(c);
+    for (unsigned i = 0; i < N; i++) {
+        s.add(x[i] >= 1);
+    }
+
+    std::cout << s << "\n" << "solving...\n" << s.check() << "\n";
+    model m = s.get_model();
+    std::cout << "solution\n" << m;
+}
+
 int main() {
     try {
         demorgan(); std::cout << "\n";
@@ -941,6 +963,7 @@ int main() {
 	incremental_example2(); std::cout << "\n";
 	incremental_example3(); std::cout << "\n";
         enum_sort_example(); std::cout << "\n";
+        expr_vector_example(); std::cout << "\n";
         std::cout << "done\n";
     }
     catch (exception & ex) {