Add SMT2 output.

main.cpp

@@ -148,19 +148,19 @@ int main(int argc, char* argv[])
     e = e.simplify();
     //std::cout << e << std::endl;
 
-    if (runZ3)
-    {
-        solver s = tactic(ctx, "bv").mk_solver();
-	params p(ctx);
+    solver s = tactic(ctx, "bv").mk_solver();
+    params p(ctx);
 
-	//	p.set(":max_memory", 3u);
-	s.set(p);
+    //	p.set(":max_memory", 3u);
+    s.set(p);
 
-	s.add(e);
+    s.add(e);
+    if (runZ3)
+    {
 	std::cout << s.check() << std::endl;
     }
     else
     {
-	std::cout << e << std::endl;
+	std::cout << s.to_smt2() << std::endl;
     }
 }