Merge pull request #106 from pcc/smtlib-printer

Modify the SMT-LIB printer to declare arrays in a deterministic (alphabetical) order.

5 files changed, 1429 insertions, 1437 deletions

diff --git a/include/klee/util/ExprSMTLIBLetPrinter.h b/include/klee/util/ExprSMTLIBLetPrinter.h
index 56c8f008..dd97e0d5 100644
--- a/include/klee/util/ExprSMTLIBLetPrinter.h
+++ b/include/klee/util/ExprSMTLIBLetPrinter.h
@@ -1,4 +1,5 @@
-//===-- ExprSMTLIBLetPrinter.h ------------------------------------------*- C++ -*-===//
+//===-- ExprSMTLIBLetPrinter.h ------------------------------------------*- C++
+//-*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -11,63 +12,62 @@
 #ifndef EXPRSMTLETPRINTER_H_
 #define EXPRSMTLETPRINTER_H_
 
-namespace klee
-{
-	/// This printer behaves like ExprSMTLIBPrinter except that it will abbreviate expressions
-	/// using the (let) SMT-LIBv2 command. Expression trees that appear two or more times in the Query
-	/// passed to setQuery() will be abbreviated.
-	///
-	/// This class should be used just like ExprSMTLIBPrinter.
-	class ExprSMTLIBLetPrinter : public ExprSMTLIBPrinter
-	{
-		public:
-			ExprSMTLIBLetPrinter();
-			virtual ~ExprSMTLIBLetPrinter() { }
-			virtual void generateOutput();
-		protected:
-			virtual void scan(const ref<Expr>& e);
-			virtual void reset();
-			virtual void generateBindings();
-			void printExpression(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort);
-			void printLetExpression();
+namespace klee {
+/// This printer behaves like ExprSMTLIBPrinter except that it will abbreviate
+/// expressions
+/// using the (let) SMT-LIBv2 command. Expression trees that appear two or more
+/// times in the Query
+/// passed to setQuery() will be abbreviated.
+///
+/// This class should be used just like ExprSMTLIBPrinter.
+class ExprSMTLIBLetPrinter : public ExprSMTLIBPrinter {
+public:
+  ExprSMTLIBLetPrinter();
+  virtual ~ExprSMTLIBLetPrinter() {}
+  virtual void generateOutput();
 
-		private:
-			///Let expression binding number map.
-			std::map<const ref<Expr>,unsigned int> bindings;
+protected:
+  virtual void scan(const ref<Expr> &e);
+  virtual void reset();
+  virtual void generateBindings();
+  void printExpression(const ref<Expr> &e,
+                       ExprSMTLIBPrinter::SMTLIB_SORT expectedSort);
+  void printLetExpression();
 
-			/* These are effectively expression counters.
-			 * firstEO - first Occurrence of expression contains
-			 *           all expressions that occur once. It is
-			 *           only used to help us fill twoOrMoreOE
-			 *
-			 * twoOrMoreEO - Contains occur all expressions that
-			 *               that occur two or more times. These
-			 *               are the expressions that will be
-			 *               abbreviated by using (let () ()) expressions.
-			 *
-			 *
-			 *
-			 */
-			std::set<ref<Expr> > firstEO, twoOrMoreEO;
+private:
+  /// Let expression binding number map.
+  std::map<const ref<Expr>, unsigned int> bindings;
 
-			///This is the prefix string used for all abbreviations in (let) expressions.
-			static const char BINDING_PREFIX[];
+  /* These are effectively expression counters.
+   * firstEO - first Occurrence of expression contains
+   *           all expressions that occur once. It is
+   *           only used to help us fill twoOrMoreOE
+   *
+   * twoOrMoreEO - Contains occur all expressions that
+   *               that occur two or more times. These
+   *               are the expressions that will be
+   *               abbreviated by using (let () ()) expressions.
+   *
+   *
+   *
+   */
+  std::set<ref<Expr> > firstEO, twoOrMoreEO;
 
-			/* This is needed during un-abbreviated printing.
-			 * Because we have overloaded printExpression()
-			 * the parent will call it and will abbreviate
-			 * when we don't want it to. This bool allows us
-			 * to switch it on/off easily.
-			 */
-			bool disablePrintedAbbreviations;
+  /// This is the prefix string used for all abbreviations in (let) expressions.
+  static const char BINDING_PREFIX[];
 
+  /* This is needed during un-abbreviated printing.
+   * Because we have overloaded printExpression()
+   * the parent will call it and will abbreviate
+   * when we don't want it to. This bool allows us
+   * to switch it on/off easily.
+   */
+  bool disablePrintedAbbreviations;
+};
 
-
-	};
-
-	///Create a SMT-LIBv2 printer based on command line options
-	///The caller is responsible for deleting the printer
-	ExprSMTLIBPrinter* createSMTLIBPrinter();
+/// Create a SMT-LIBv2 printer based on command line options
+/// The caller is responsible for deleting the printer
+ExprSMTLIBPrinter *createSMTLIBPrinter();
 }
 
 #endif /* EXPRSMTLETPRINTER_H_ */
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h
index 83f48eb6..42f38007 100644
--- a/include/klee/util/ExprSMTLIBPrinter.h
+++ b/include/klee/util/ExprSMTLIBPrinter.h
@@ -1,4 +1,5 @@
-//===-- ExprSMTLIBPrinter.h ------------------------------------------*- C++ -*-===//
+//===-- ExprSMTLIBPrinter.h ------------------------------------------*- C++
+//-*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -21,302 +22,324 @@
 
 namespace klee {
 
-  ///Base Class for SMTLIBv2 printer for KLEE Queries. It uses the QF_ABV logic. Note however the logic can be
-  ///set to QF_AUFBV because some solvers (e.g. STP) complain if this logic is set to QF_ABV.
+/// Base Class for SMTLIBv2 printer for KLEE Queries. It uses the QF_ABV logic.
+/// Note however the logic can be
+/// set to QF_AUFBV because some solvers (e.g. STP) complain if this logic is
+/// set to QF_ABV.
+///
+/// This printer does not abbreviate expressions. The printer
+/// ExprSMTLIBLetPrinter does though.
+///
+/// It is intended to be used as follows
+/// -# Create instance of this class
+/// -# Set output ( setOutput() )
+/// -# Set query to print ( setQuery() )
+/// -# Set options using the methods prefixed with the word "set".
+/// -# Call generateOutput()
+///
+/// The class can then be used again on another query ( setQuery() ).
+/// The options set are persistent across queries (apart from
+/// setArrayValuesToGet() and PRODUCE_MODELS).
+///
+///
+/// Note that in KLEE at the lowest level the solver checks for validity of the
+/// query, i.e.
+///
+/// \f[ \forall X constraints(X) \to query(X) \f]
+///
+/// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints
+/// in the query and \f$query(X)\f$ is the query expression.
+/// If the above formula is true the query is said to be **valid**, otherwise it
+/// is
+/// **invalid**.
+///
+/// The SMTLIBv2 language works in terms of satisfiability rather than validity
+/// so instead
+/// this class must ask the equivalent query but in terms of satisfiability
+/// which is:
+///
+/// \f[ \lnot \exists X constraints(X) \land \lnot query(X) \f]
+///
+/// The printed SMTLIBv2 query actually asks the following:
+///
+///  \f[ \exists X constraints(X) \land \lnot query(X) \f]
+/// Hence the printed SMTLIBv2 query will just assert the constraints and the
+/// negation
+/// of the query expression.
+///
+/// If a SMTLIBv2 solver says the printed query is satisfiable the then original
+/// query passed to this class was **invalid** and if a SMTLIBv2 solver says the
+/// printed
+/// query is unsatisfiable then the original query passed to this class was
+/// **valid**.
+///
+class ExprSMTLIBPrinter {
+public:
+  /// Different SMTLIBv2 logics supported by this class
+  /// \sa setLogic()
+  enum SMTLIBv2Logic {
+    QF_ABV,  ///< Logic using Theory of Arrays and Theory of Bitvectors
+    QF_AUFBV ///< Logic using Theory of Arrays and Theory of Bitvectors and has
+             ///uninterpreted functions
+  };
+
+  /// Different SMTLIBv2 options that have a boolean value that can be set
+  /// \sa setSMTLIBboolOption
+  enum SMTLIBboolOptions {
+    PRINT_SUCCESS,   ///< print-success SMTLIBv2 option
+    PRODUCE_MODELS,  ///< produce-models SMTLIBv2 option
+    INTERACTIVE_MODE ///< interactive-mode SMTLIBv2 option
+  };
+
+  /// Different SMTLIBv2 bool option values
+  /// \sa setSMTLIBboolOption
+  enum SMTLIBboolValues {
+    OPTION_TRUE,   ///< Set option to true
+    OPTION_FALSE,  ///< Set option to false
+    OPTION_DEFAULT ///< Use solver's defaults (the option will not be set in
+                   ///output)
+  };
+
+  enum ConstantDisplayMode {
+    BINARY, ///< Display bit vector constants in binary e.g. #b00101101
+    HEX,    ///< Display bit vector constants in Hexidecimal e.g.#x2D
+    DECIMAL ///< Display bit vector constants in Decimal e.g. (_ bv45 8)
+  };
+
+  /// Different supported SMTLIBv2 sorts (a.k.a type) in QF_AUFBV
+  enum SMTLIB_SORT { SORT_BITVECTOR, SORT_BOOL };
+
+  /// Allows the way Constant bitvectors are printed to be changed.
+  /// This setting is persistent across queries.
+  /// \return true if setting the mode was successful
+  bool setConstantDisplayMode(ConstantDisplayMode cdm);
+
+  ConstantDisplayMode getConstantDisplayMode() { return cdm; }
+
+  /// Create a new printer that will print a query in the SMTLIBv2 language.
+  ExprSMTLIBPrinter();
+
+  /// Set the output stream that will be printed to.
+  /// This call is persistent across queries.
+  void setOutput(std::ostream &output);
+
+  /// Set the query to print. This will setArrayValuesToGet()
+  /// to none (i.e. no array values will be requested using
+  /// the SMTLIBv2 (get-value ()) command).
+  void setQuery(const Query &q);
+
+  virtual ~ExprSMTLIBPrinter();
+
+  /// Print the query to the std::ostream
+  /// setOutput() and setQuery() must be called before calling this.
   ///
-  ///This printer does not abbreviate expressions. The printer ExprSMTLIBLetPrinter does though.
+  /// All options should be set before calling this.
+  /// \sa setConstantDisplayMode
+  /// \sa setLogic()
+  /// \sa setHumanReadable
+  /// \sa setSMTLIBboolOption
+  /// \sa setArrayValuesToGet
   ///
-  /// It is intended to be used as follows
-  /// -# Create instance of this class
-  /// -# Set output ( setOutput() )
-  /// -# Set query to print ( setQuery() )
-  /// -# Set options using the methods prefixed with the word "set".
-  /// -# Call generateOutput()
+  /// Mostly it does not matter what order the options are set in. However
+  /// calling
+  /// setArrayValuesToGet() implies PRODUCE_MODELS is set so, if a call to
+  /// setSMTLIBboolOption()
+  /// is made that uses the PRODUCE_MODELS before calling setArrayValuesToGet()
+  /// then the setSMTLIBboolOption()
+  /// call will be ineffective.
+  virtual void generateOutput();
+
+  /// Set which SMTLIBv2 logic to use.
+  /// This only affects what logic is used in the (set-logic <logic>) command.
+  /// The rest of the printed SMTLIBv2 commands are the same regardless of the
+  /// logic used.
   ///
-  ///The class can then be used again on another query ( setQuery() ).
-  ///The options set are persistent across queries (apart from setArrayValuesToGet() and PRODUCE_MODELS).
-  ///
-  ///
-  ///Note that in KLEE at the lowest level the solver checks for validity of the query, i.e.
-  ///
-  /// \f[ \forall X constraints(X) \to query(X) \f]
-  ///
-  /// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints
-  /// in the query and \f$query(X)\f$ is the query expression.
-  /// If the above formula is true the query is said to be **valid**, otherwise it is
-  /// **invalid**.
+  /// \return true if setting logic was successful.
+  bool setLogic(SMTLIBv2Logic l);
+
+  /// Sets how readable the printed SMTLIBv2 commands are.
+  /// \param hr If set to true the printed commands are made more human
+  /// readable.
   ///
-  /// The SMTLIBv2 language works in terms of satisfiability rather than validity so instead
-  /// this class must ask the equivalent query but in terms of satisfiability which is:
+  /// The printed commands are made human readable by...
+  /// - Indenting and line breaking.
+  /// - Adding comments
+  void setHumanReadable(bool hr);
+
+  /// Set SMTLIB options.
+  /// These options will be printed when generateOutput() is called via
+  /// the SMTLIBv2 command (set-option :option-name <value>)
   ///
-  /// \f[ \lnot \exists X constraints(X) \land \lnot query(X) \f]
+  /// By default no options will be printed so the SMTLIBv2 solver will use
+  /// its default values for all options.
   ///
-  /// The printed SMTLIBv2 query actually asks the following:
+  /// \return true if option was successfully set.
   ///
-  ///  \f[ \exists X constraints(X) \land \lnot query(X) \f]
-  /// Hence the printed SMTLIBv2 query will just assert the constraints and the negation
-  /// of the query expression.
+  /// The options set are persistent across calls to setQuery() apart from the
+  /// PRODUCE_MODELS option which this printer may automatically set/unset.
+  bool setSMTLIBboolOption(SMTLIBboolOptions option, SMTLIBboolValues value);
+
+  /// Set the array names that the SMTLIBv2 solver will be asked to determine.
+  /// Calling this method implies the PRODUCE_MODELS option is true and will
+  /// change
+  /// any previously set value.
   ///
-  /// If a SMTLIBv2 solver says the printed query is satisfiable the then original
-  /// query passed to this class was **invalid** and if a SMTLIBv2 solver says the printed
-  /// query is unsatisfiable then the original query passed to this class was **valid**.
+  /// If no call is made to this function before
+  /// ExprSMTLIBPrinter::generateOutput() then
+  /// the solver will only be asked to check satisfiability.
   ///
-	class ExprSMTLIBPrinter
-	{
-		public:
-
-			///Different SMTLIBv2 logics supported by this class
-			/// \sa setLogic()
-			enum SMTLIBv2Logic
-			{
-				QF_ABV,  ///< Logic using Theory of Arrays and Theory of Bitvectors
-				QF_AUFBV ///< Logic using Theory of Arrays and Theory of Bitvectors and has uninterpreted functions
-			};
-
-			///Different SMTLIBv2 options that have a boolean value that can be set
-			/// \sa setSMTLIBboolOption
-			enum SMTLIBboolOptions
-			{
-				PRINT_SUCCESS, ///< print-success SMTLIBv2 option
-				PRODUCE_MODELS,///< produce-models SMTLIBv2 option
-				INTERACTIVE_MODE ///< interactive-mode SMTLIBv2 option
-			};
-
-			///Different SMTLIBv2 bool option values
-			/// \sa setSMTLIBboolOption
-			enum SMTLIBboolValues
-			{
-				OPTION_TRUE, ///< Set option to true
-				OPTION_FALSE, ///< Set option to false
-				OPTION_DEFAULT ///< Use solver's defaults (the option will not be set in output)
-			};
-
-			enum ConstantDisplayMode
-			{
-				BINARY,///< Display bit vector constants in binary e.g. #b00101101
-				HEX, ///< Display bit vector constants in Hexidecimal e.g.#x2D
-				DECIMAL ///< Display bit vector constants in Decimal e.g. (_ bv45 8)
-			};
-
-			///Different supported SMTLIBv2 sorts (a.k.a type) in QF_AUFBV
-			enum SMTLIB_SORT
-			{
-				SORT_BITVECTOR,
-				SORT_BOOL
-			};
-
-
-
-			///Allows the way Constant bitvectors are printed to be changed.
-			///This setting is persistent across queries.
-			/// \return true if setting the mode was successful
-			bool setConstantDisplayMode(ConstantDisplayMode cdm);
-
-			ConstantDisplayMode getConstantDisplayMode() { return cdm;}
-
-			///Create a new printer that will print a query in the SMTLIBv2 language.
-			ExprSMTLIBPrinter();
-
-			///Set the output stream that will be printed to.
-			///This call is persistent across queries.
-			void setOutput(std::ostream& output);
-
-			///Set the query to print. This will setArrayValuesToGet()
-			///to none (i.e. no array values will be requested using
-			///the SMTLIBv2 (get-value ()) command).
-			void setQuery(const Query& q);
-
-			virtual ~ExprSMTLIBPrinter();
-
-			/// Print the query to the std::ostream
-			/// setOutput() and setQuery() must be called before calling this.
-			///
-			/// All options should be set before calling this.
-			/// \sa setConstantDisplayMode
-			/// \sa setLogic()
-			/// \sa setHumanReadable
-			/// \sa setSMTLIBboolOption
-			/// \sa setArrayValuesToGet
-			///
-			/// Mostly it does not matter what order the options are set in. However calling
-			/// setArrayValuesToGet() implies PRODUCE_MODELS is set so, if a call to setSMTLIBboolOption()
-			/// is made that uses the PRODUCE_MODELS before calling setArrayValuesToGet() then the setSMTLIBboolOption()
-			/// call will be ineffective.
-			virtual void generateOutput();
-
-			///Set which SMTLIBv2 logic to use.
-			///This only affects what logic is used in the (set-logic <logic>) command.
-			///The rest of the printed SMTLIBv2 commands are the same regardless of the logic used.
-			///
-			/// \return true if setting logic was successful.
-			bool setLogic(SMTLIBv2Logic l);
-
-			///Sets how readable the printed SMTLIBv2 commands are.
-			/// \param hr If set to true the printed commands are made more human readable.
-			///
-			/// The printed commands are made human readable by...
-			/// - Indenting and line breaking.
-			/// - Adding comments
-			void setHumanReadable(bool hr);
-
-			///Set SMTLIB options.
-			/// These options will be printed when generateOutput() is called via
-			/// the SMTLIBv2 command (set-option :option-name <value>)
-			///
-			/// By default no options will be printed so the SMTLIBv2 solver will use
-			/// its default values for all options.
-			///
-			/// \return true if option was successfully set.
-			///
-			/// The options set are persistent across calls to setQuery() apart from the
-			/// PRODUCE_MODELS option which this printer may automatically set/unset.
-			bool setSMTLIBboolOption(SMTLIBboolOptions option, SMTLIBboolValues value);
-
-			/// Set the array names that the SMTLIBv2 solver will be asked to determine.
-			/// Calling this method implies the PRODUCE_MODELS option is true and will change
-			/// any previously set value.
-			///
-			/// If no call is made to this function before ExprSMTLIBPrinter::generateOutput() then
-			/// the solver will only be asked to check satisfiability.
-			///
-			/// If the passed vector is not empty then the values of those arrays will be requested
-			/// via (get-value ()) SMTLIBv2 command in the output stream in the same order as vector.
-			void setArrayValuesToGet(const std::vector<const Array*>& a);
-
-			/// \return True if human readable mode is switched on
-			bool isHumanReadable();
-
-
-		protected:
-			///Contains the arrays found during scans
-			std::set<const Array*> usedArrays;
-
-			///Output stream to write to
-			std::ostream* o;
-
-			///The query to print
-			const Query* query;
-
-			///Determine the SMTLIBv2 sort of the expression
-			SMTLIB_SORT getSort(const ref<Expr>& e);
-
-			///Print an expression but cast it to a particular SMTLIBv2 sort first.
-			void printCastToSort(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT sort);
-
-			//Resets various internal objects for a new query
-			virtual void reset();
-
-			//Scan all constraints and the query
-			virtual void scanAll();
-
-			//Print an initial SMTLIBv2 comment before anything else is printed
-			virtual void printNotice();
-
-			//Print SMTLIBv2 options e.g. (set-option :option-name <value>) command
-			virtual void printOptions();
-
-			//Print SMTLIBv2 logic to use e.g. (set-logic QF_ABV)
-			virtual void printSetLogic();
-
-			//Print SMTLIBv2 assertions for constant arrays
-			virtual void printArrayDeclarations();
-
-			//Print SMTLIBv2 for all constraints in the query
-			virtual void printConstraints();
-
-			//Print SMTLIBv2 assert statement for the negated query expression
-			virtual void printQuery();
-
-			///Print the SMTLIBv2 command to check satisfiability and also optionally request for values
-			/// \sa setArrayValuesToGet()
-			virtual void printAction();
-
-			///Print the SMTLIBv2 command to exit
-			virtual void printExit();
-
-			///Print a Constant in the format specified by the current "Constant Display Mode"
-			void printConstant(const ref<ConstantExpr>& e);
-
-			///Recursively print expression
-			/// \param e is the expression to print
-			/// \param expectedSort is the sort we want. If "e" is not of the right type a cast will be performed.
-			virtual void printExpression(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort);
-
-			///Scan Expression recursively for Arrays in expressions. Found arrays are added to
-			/// the usedArrays vector.
-			virtual void scan(const ref<Expr>& e);
-
-			/* Rules of recursion for "Special Expression handlers" and printSortArgsExpr()
-			 *
-			 * 1. The parent of the recursion will have created an indent level for you so you don't need to add another initially.
-			 * 2. You do not need to add a line break (via printSeperator() ) at the end, the parent caller will handle that.
-			 * 3. The effect of a single recursive call should not affect the depth of the indent stack (nor the contents
-			 *    of the indent stack prior to the call). I.e. After executing a single recursive call the indent stack
-			 *    should have the same size and contents as before executing the recursive call.
-			 */
-
-			//Special Expression handlers
-			virtual void printReadExpr(const ref<ReadExpr>& e);
-			virtual void printExtractExpr(const ref<ExtractExpr>& e);
-			virtual void printCastExpr(const ref<CastExpr>& e);
-			virtual void printNotEqualExpr(const ref<NeExpr>& e);
-			virtual void printSelectExpr(const ref<SelectExpr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s);
-
-			//For the set of operators that take sort "s" arguments
-			virtual void printSortArgsExpr(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s);
-
-			///For the set of operators that come in two sorts (e.g. (and () ()) (bvand () ()) )
-			///These are and,xor,or,not
-			/// \param e the Expression to print
-			/// \param s the sort of the expression we want
-			virtual void printLogicalOrBitVectorExpr(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s);
-
-			///Recursively prints updatesNodes
-			virtual void printUpdatesAndArray(const UpdateNode* un, const Array* root);
-
-			///This method does the translation between Expr classes and SMTLIBv2 keywords
-			/// \return A C-string of the SMTLIBv2 keyword
-			virtual const char* getSMTLIBKeyword(const ref<Expr>& e);
-
-			virtual void printSeperator();
-
-			///Helper function for scan() that scans the expressions of an update node
-			virtual void scanUpdates(const UpdateNode* un);
-
-			///Helper printer class
-			PrintContext* p;
-
-			///This contains the query from the solver but negated for our purposes.
-			/// \sa negateQueryExpression()
-			ref<Expr> queryAssert;
-
-			///Indicates if there were any constant arrays founds during a scan()
-			bool haveConstantArray;
-
-
-		private:
-			SMTLIBv2Logic logicToUse;
-
-			volatile bool humanReadable;
-
-			//Map of enabled SMTLIB Options
-			std::map<SMTLIBboolOptions,bool> smtlibBoolOptions;
-
-			///This sets queryAssert to be the boolean negation of the original Query
-			void negateQueryExpression();
-
-			//Print a SMTLIBv2 option as a C-string
-			const char* getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option);
+  /// If the passed vector is not empty then the values of those arrays will be
+  /// requested
+  /// via (get-value ()) SMTLIBv2 command in the output stream in the same order
+  /// as vector.
+  void setArrayValuesToGet(const std::vector<const Array *> &a);
+
+  /// \return True if human readable mode is switched on
+  bool isHumanReadable();
+
+protected:
+  /// Contains the arrays found during scans
+  std::set<const Array *> usedArrays;
+
+  /// Output stream to write to
+  std::ostream *o;
+
+  /// The query to print
+  const Query *query;
+
+  /// Determine the SMTLIBv2 sort of the expression
+  SMTLIB_SORT getSort(const ref<Expr> &e);
+
+  /// Print an expression but cast it to a particular SMTLIBv2 sort first.
+  void printCastToSort(const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT sort);
+
+  // Resets various internal objects for a new query
+  virtual void reset();
+
+  // Scan all constraints and the query
+  virtual void scanAll();
+
+  // Print an initial SMTLIBv2 comment before anything else is printed
+  virtual void printNotice();
+
+  // Print SMTLIBv2 options e.g. (set-option :option-name <value>) command
+  virtual void printOptions();
+
+  // Print SMTLIBv2 logic to use e.g. (set-logic QF_ABV)
+  virtual void printSetLogic();
+
+  // Print SMTLIBv2 assertions for constant arrays
+  virtual void printArrayDeclarations();
 
-			//Pointer to a vector of Arrays. These will be used for the (get-value () ) call.
-			const std::vector<const Array*> * arraysToCallGetValueOn;
+  // Print SMTLIBv2 for all constraints in the query
+  virtual void printConstraints();
 
-			ConstantDisplayMode cdm;
+  // Print SMTLIBv2 assert statement for the negated query expression
+  virtual void printQuery();
+
+  /// Print the SMTLIBv2 command to check satisfiability and also optionally
+  /// request for values
+  /// \sa setArrayValuesToGet()
+  virtual void printAction();
+
+  /// Print the SMTLIBv2 command to exit
+  virtual void printExit();
+
+  /// Print a Constant in the format specified by the current "Constant Display
+  /// Mode"
+  void printConstant(const ref<ConstantExpr> &e);
+
+  /// Recursively print expression
+  /// \param e is the expression to print
+  /// \param expectedSort is the sort we want. If "e" is not of the right type a
+  /// cast will be performed.
+  virtual void printExpression(const ref<Expr> &e,
+                               ExprSMTLIBPrinter::SMTLIB_SORT expectedSort);
+
+  /// Scan Expression recursively for Arrays in expressions. Found arrays are
+  /// added to
+  /// the usedArrays vector.
+  virtual void scan(const ref<Expr> &e);
+
+  /* Rules of recursion for "Special Expression handlers" and
+   *printSortArgsExpr()
+   *
+   * 1. The parent of the recursion will have created an indent level for you so
+   *you don't need to add another initially.
+   * 2. You do not need to add a line break (via printSeperator() ) at the end,
+   *the parent caller will handle that.
+   * 3. The effect of a single recursive call should not affect the depth of the
+   *indent stack (nor the contents
+   *    of the indent stack prior to the call). I.e. After executing a single
+   *recursive call the indent stack
+   *    should have the same size and contents as before executing the recursive
+   *call.
+   */
+
+  // Special Expression handlers
+  virtual void printReadExpr(const ref<ReadExpr> &e);
+  virtual void printExtractExpr(const ref<ExtractExpr> &e);
+  virtual void printCastExpr(const ref<CastExpr> &e);
+  virtual void printNotEqualExpr(const ref<NeExpr> &e);
+  virtual void printSelectExpr(const ref<SelectExpr> &e,
+                               ExprSMTLIBPrinter::SMTLIB_SORT s);
+
+  // For the set of operators that take sort "s" arguments
+  virtual void printSortArgsExpr(const ref<Expr> &e,
+                                 ExprSMTLIBPrinter::SMTLIB_SORT s);
+
+  /// For the set of operators that come in two sorts (e.g. (and () ()) (bvand
+  /// () ()) )
+  /// These are and,xor,or,not
+  /// \param e the Expression to print
+  /// \param s the sort of the expression we want
+  virtual void printLogicalOrBitVectorExpr(const ref<Expr> &e,
+                                           ExprSMTLIBPrinter::SMTLIB_SORT s);
 
-	};
+  /// Recursively prints updatesNodes
+  virtual void printUpdatesAndArray(const UpdateNode *un, const Array *root);
 
+  /// This method does the translation between Expr classes and SMTLIBv2
+  /// keywords
+  /// \return A C-string of the SMTLIBv2 keyword
+  virtual const char *getSMTLIBKeyword(const ref<Expr> &e);
 
+  virtual void printSeperator();
 
+  /// Helper function for scan() that scans the expressions of an update node
+  virtual void scanUpdates(const UpdateNode *un);
+
+  /// Helper printer class
+  PrintContext *p;
+
+  /// This contains the query from the solver but negated for our purposes.
+  /// \sa negateQueryExpression()
+  ref<Expr> queryAssert;
+
+  /// Indicates if there were any constant arrays founds during a scan()
+  bool haveConstantArray;
+
+private:
+  SMTLIBv2Logic logicToUse;
+
+  volatile bool humanReadable;
+
+  // Map of enabled SMTLIB Options
+  std::map<SMTLIBboolOptions, bool> smtlibBoolOptions;
+
+  /// This sets queryAssert to be the boolean negation of the original Query
+  void negateQueryExpression();
+
+  // Print a SMTLIBv2 option as a C-string
+  const char *
+  getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option);
+
+  // Pointer to a vector of Arrays. These will be used for the (get-value () )
+  // call.
+  const std::vector<const Array *> *arraysToCallGetValueOn;
+
+  ConstantDisplayMode cdm;
+};
 }
 
 #endif
diff --git a/lib/Expr/ExprSMTLIBLetPrinter.cpp b/lib/Expr/ExprSMTLIBLetPrinter.cpp
index 7225704e..6a88ab5d 100644
--- a/lib/Expr/ExprSMTLIBLetPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBLetPrinter.cpp
@@ -1,4 +1,5 @@
-//===-- ExprSMTLIBLetPrinter.cpp ------------------------------------------*- C++ -*-===//
+//===-- ExprSMTLIBLetPrinter.cpp ------------------------------------------*-
+//C++ -*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -13,237 +14,220 @@
 
 using namespace std;
 
-namespace ExprSMTLIBOptions
-{
-	llvm::cl::opt<bool> useLetExpressions("smtlib-use-let-expressions",
-			llvm::cl::desc("Enables generated SMT-LIBv2 files to use (let) expressions (default=on)"),
-			llvm::cl::init(true)
-	);
+namespace ExprSMTLIBOptions {
+llvm::cl::opt<bool>
+useLetExpressions("smtlib-use-let-expressions",
+                  llvm::cl::desc("Enables generated SMT-LIBv2 files to use "
+                                 "(let) expressions (default=on)"),
+                  llvm::cl::init(true));
 }
 
-namespace klee
-{
-	const char ExprSMTLIBLetPrinter::BINDING_PREFIX[] = "?B";
-
-
-	ExprSMTLIBLetPrinter::ExprSMTLIBLetPrinter() :
-	bindings(), firstEO(), twoOrMoreEO(),
-	disablePrintedAbbreviations(false)
-	{
-	}
-
-	void ExprSMTLIBLetPrinter::generateOutput()
-	{
-		if(p==NULL || query == NULL || o ==NULL)
-		{
-			std::cerr << "Can't print SMTLIBv2. Output or query bad!" << std::endl;
-			return;
-		}
-
-		generateBindings();
-
-		if(isHumanReadable()) printNotice();
-		printOptions();
-		printSetLogic();
-		printArrayDeclarations();
-		printLetExpression();
-		printAction();
-		printExit();
-	}
-
-	void ExprSMTLIBLetPrinter::scan(const ref<Expr>& e)
-	{
-		if(isa<ConstantExpr>(e))
-			return; //we don't need to scan simple constants
-
-		if(firstEO.insert(e).second)
-		{
-			//We've not seen this expression before
-
-			if(const ReadExpr* re = dyn_cast<ReadExpr>(e))
-			{
-
-				//Attempt to insert array and if array wasn't present before do more things
-				if(usedArrays.insert(re->updates.root).second)
-				{
-
-					//check if the array is constant
-					if( re->updates.root->isConstantArray())
-						haveConstantArray=true;
-
-					//scan the update list
-					scanUpdates(re->updates.head);
-
-				}
-
-			}
-
-			//recurse into the children
-			Expr* ep = e.get();
-			for(unsigned int i=0; i < ep->getNumKids(); i++)
-				scan(ep->getKid(i));
-		}
-		else
-		{
-			/* We must of seen the expression before. Add it to
-			 * the set of twoOrMoreOccurances. We don't need to
-			 * check if the insertion fails.
-			 */
-			twoOrMoreEO.insert(e);
-		}
-	}
-
-	void ExprSMTLIBLetPrinter::generateBindings()
-	{
-		//Assign a number to each binding that will be used
-		unsigned int counter=0;
-		for(set<ref<Expr> >::const_iterator i=twoOrMoreEO.begin();
-				i!= twoOrMoreEO.end(); ++i)
-		{
-			bindings.insert(std::make_pair(*i,counter));
-			++counter;
-		}
-	}
-
-	void ExprSMTLIBLetPrinter::printExpression(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort)
-	{
-		map<const ref<Expr>,unsigned int>::const_iterator i= bindings.find(e);
-
-		if(disablePrintedAbbreviations || i == bindings.end())
-		{
-			/*There is no abbreviation for this expression so print it normally.
-			 * Do this by using the parent method.
-			 */
-			ExprSMTLIBPrinter::printExpression(e,expectedSort);
-		}
-		else
-		{
-			//Use binding name e.g. "?B1"
-
-			/* Handle the corner case where the expectedSort
-			 * doesn't match the sort of the abbreviation. Not really very efficient (calls bindings.find() twice),
-			 * we'll cast and call ourself again but with the correct expectedSort.
-			 */
-			if(getSort(e) != expectedSort)
-			{
-				printCastToSort(e,expectedSort);
-				return;
-			}
-
-			// No casting is needed in this depth of recursion, just print the abbreviation
-			*p << BINDING_PREFIX << i->second;
-		}
-	}
-
-	void ExprSMTLIBLetPrinter::reset()
-	{
-		//Let parent clean up first
-		ExprSMTLIBPrinter::reset();
-
-		firstEO.clear();
-		twoOrMoreEO.clear();
-		bindings.clear();
-	}
-
-	void ExprSMTLIBLetPrinter::printLetExpression()
-	{
-		*p << "(assert"; p->pushIndent(); printSeperator();
-
-		if(bindings.size() !=0 )
-		{
-			//Only print let expression if we have bindings to use.
-			*p << "(let"; p->pushIndent(); printSeperator();
-			*p << "( "; p->pushIndent();
-
-			//Print each binding
-			for(map<const ref<Expr>, unsigned int>::const_iterator i= bindings.begin();
-					i!=bindings.end(); ++i)
-			{
-				printSeperator();
-				*p << "(" << BINDING_PREFIX << i->second << " ";
-				p->pushIndent();
-
-				//Disable abbreviations so none are used here.
-				disablePrintedAbbreviations=true;
-
-				//We can abbreviate SORT_BOOL or SORT_BITVECTOR in let expressions
-				printExpression(i->first,getSort(i->first));
-
-				p->popIndent();
-				printSeperator();
-				*p << ")";
-			}
-
-
-			p->popIndent(); printSeperator();
-			*p << ")";
-			printSeperator();
-
-			//Re-enable printing abbreviations.
-			disablePrintedAbbreviations=false;
-
-		}
-
-		//print out Expressions with abbreviations.
-		unsigned int numberOfItems= query->constraints.size() +1; //+1 for query
-		unsigned int itemsLeft=numberOfItems;
-		vector<ref<Expr> >::const_iterator constraint=query->constraints.begin();
-
-		/* Produce nested (and () () statements. If the constraint set
-		 * is empty then we will only print the "queryAssert".
-		 */
-		for(; itemsLeft !=0; --itemsLeft)
-		{
-			if(itemsLeft >=2)
-			{
-				*p << "(and"; p->pushIndent(); printSeperator();
-				printExpression(*constraint,SORT_BOOL); //We must and together bool expressions
-				printSeperator();
-				++constraint;
-				continue;
-			}
-			else
-			{
-				// must have 1 item left (i.e. the "queryAssert")
-				if(isHumanReadable()) { *p << "; query"; p->breakLineI();}
-				printExpression(queryAssert,SORT_BOOL); //The query must be a bool expression
-
-			}
-		}
-
-		/* Produce closing brackets for nested "and statements".
-		 * Number of "nested ands" = numberOfItems -1
-		 */
-		itemsLeft= numberOfItems -1;
-		for(; itemsLeft!=0; --itemsLeft)
-		{
-			p->popIndent(); printSeperator();
-			*p << ")";
-		}
-
-
-
-		if(bindings.size() !=0)
-		{
-			//end let expression
-			p->popIndent(); printSeperator();
-			*p << ")";  printSeperator();
-		}
-
-		//end assert
-		p->popIndent(); printSeperator();
-		*p << ")";
-		p->breakLineI();
-	}
-
-	ExprSMTLIBPrinter* createSMTLIBPrinter()
-	{
-		if(ExprSMTLIBOptions::useLetExpressions)
-			return new ExprSMTLIBLetPrinter();
-		else
-			return new ExprSMTLIBPrinter();
-	}
+namespace klee {
+const char ExprSMTLIBLetPrinter::BINDING_PREFIX[] = "?B";
 
+ExprSMTLIBLetPrinter::ExprSMTLIBLetPrinter()
+    : bindings(), firstEO(), twoOrMoreEO(), disablePrintedAbbreviations(false) {
+}
+
+void ExprSMTLIBLetPrinter::generateOutput() {
+  if (p == NULL || query == NULL || o == NULL) {
+    std::cerr << "Can't print SMTLIBv2. Output or query bad!" << std::endl;
+    return;
+  }
+
+  generateBindings();
+
+  if (isHumanReadable())
+    printNotice();
+  printOptions();
+  printSetLogic();
+  printArrayDeclarations();
+  printLetExpression();
+  printAction();
+  printExit();
+}
+
+void ExprSMTLIBLetPrinter::scan(const ref<Expr> &e) {
+  if (isa<ConstantExpr>(e))
+    return; // we don't need to scan simple constants
+
+  if (firstEO.insert(e).second) {
+    // We've not seen this expression before
+
+    if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
+
+      // Attempt to insert array and if array wasn't present before do more
+      // things
+      if (usedArrays.insert(re->updates.root).second) {
+
+        // check if the array is constant
+        if (re->updates.root->isConstantArray())
+          haveConstantArray = true;
+
+        // scan the update list
+        scanUpdates(re->updates.head);
+      }
+    }
+
+    // recurse into the children
+    Expr *ep = e.get();
+    for (unsigned int i = 0; i < ep->getNumKids(); i++)
+      scan(ep->getKid(i));
+  } else {
+    /* We must of seen the expression before. Add it to
+     * the set of twoOrMoreOccurances. We don't need to
+     * check if the insertion fails.
+     */
+    twoOrMoreEO.insert(e);
+  }
+}
+
+void ExprSMTLIBLetPrinter::generateBindings() {
+  // Assign a number to each binding that will be used
+  unsigned int counter = 0;
+  for (set<ref<Expr> >::const_iterator i = twoOrMoreEO.begin();
+       i != twoOrMoreEO.end(); ++i) {
+    bindings.insert(std::make_pair(*i, counter));
+    ++counter;
+  }
+}
 
+void ExprSMTLIBLetPrinter::printExpression(
+    const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) {
+  map<const ref<Expr>, unsigned int>::const_iterator i = bindings.find(e);
+
+  if (disablePrintedAbbreviations || i == bindings.end()) {
+    /*There is no abbreviation for this expression so print it normally.
+     * Do this by using the parent method.
+     */
+    ExprSMTLIBPrinter::printExpression(e, expectedSort);
+  } else {
+    // Use binding name e.g. "?B1"
+
+    /* Handle the corner case where the expectedSort
+     * doesn't match the sort of the abbreviation. Not really very efficient
+     * (calls bindings.find() twice),
+     * we'll cast and call ourself again but with the correct expectedSort.
+     */
+    if (getSort(e) != expectedSort) {
+      printCastToSort(e, expectedSort);
+      return;
+    }
+
+    // No casting is needed in this depth of recursion, just print the
+    // abbreviation
+    *p << BINDING_PREFIX << i->second;
+  }
 }
 
+void ExprSMTLIBLetPrinter::reset() {
+  // Let parent clean up first
+  ExprSMTLIBPrinter::reset();
+
+  firstEO.clear();
+  twoOrMoreEO.clear();
+  bindings.clear();
+}
+
+void ExprSMTLIBLetPrinter::printLetExpression() {
+  *p << "(assert";
+  p->pushIndent();
+  printSeperator();
+
+  if (bindings.size() != 0) {
+    // Only print let expression if we have bindings to use.
+    *p << "(let";
+    p->pushIndent();
+    printSeperator();
+    *p << "( ";
+    p->pushIndent();
+
+    // Print each binding
+    for (map<const ref<Expr>, unsigned int>::const_iterator i =
+             bindings.begin();
+         i != bindings.end(); ++i) {
+      printSeperator();
+      *p << "(" << BINDING_PREFIX << i->second << " ";
+      p->pushIndent();
+
+      // Disable abbreviations so none are used here.
+      disablePrintedAbbreviations = true;
+
+      // We can abbreviate SORT_BOOL or SORT_BITVECTOR in let expressions
+      printExpression(i->first, getSort(i->first));
+
+      p->popIndent();
+      printSeperator();
+      *p << ")";
+    }
+
+    p->popIndent();
+    printSeperator();
+    *p << ")";
+    printSeperator();
+
+    // Re-enable printing abbreviations.
+    disablePrintedAbbreviations = false;
+  }
+
+  // print out Expressions with abbreviations.
+  unsigned int numberOfItems = query->constraints.size() + 1; //+1 for query
+  unsigned int itemsLeft = numberOfItems;
+  vector<ref<Expr> >::const_iterator constraint = query->constraints.begin();
+
+  /* Produce nested (and () () statements. If the constraint set
+   * is empty then we will only print the "queryAssert".
+   */
+  for (; itemsLeft != 0; --itemsLeft) {
+    if (itemsLeft >= 2) {
+      *p << "(and";
+      p->pushIndent();
+      printSeperator();
+      printExpression(*constraint,
+                      SORT_BOOL); // We must and together bool expressions
+      printSeperator();
+      ++constraint;
+      continue;
+    } else {
+      // must have 1 item left (i.e. the "queryAssert")
+      if (isHumanReadable()) {
+        *p << "; query";
+        p->breakLineI();
+      }
+      printExpression(queryAssert,
+                      SORT_BOOL); // The query must be a bool expression
+    }
+  }
+
+  /* Produce closing brackets for nested "and statements".
+   * Number of "nested ands" = numberOfItems -1
+   */
+  itemsLeft = numberOfItems - 1;
+  for (; itemsLeft != 0; --itemsLeft) {
+    p->popIndent();
+    printSeperator();
+    *p << ")";
+  }
+
+  if (bindings.size() != 0) {
+    // end let expression
+    p->popIndent();
+    printSeperator();
+    *p << ")";
+    printSeperator();
+  }
+
+  // end assert
+  p->popIndent();
+  printSeperator();
+  *p << ")";
+  p->breakLineI();
+}
+
+ExprSMTLIBPrinter *createSMTLIBPrinter() {
+  if (ExprSMTLIBOptions::useLetExpressions)
+    return new ExprSMTLIBLetPrinter();
+  else
+    return new ExprSMTLIBPrinter();
+}
+}
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index 9e97a4e0..c32b5bf9 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -1,4 +1,5 @@
-//===-- ExprSMTLIBPrinter.cpp ------------------------------------------*- C++ -*-===//
+//===-- ExprSMTLIBPrinter.cpp ------------------------------------------*- C++
+//-*-===//
 //
 //                     The KLEE Symbolic Virtual Machine
 //
@@ -14,893 +15,877 @@
 
 using namespace std;
 
-namespace ExprSMTLIBOptions
-{
-	//Command line options
-	llvm::cl::opt<klee::ExprSMTLIBPrinter::ConstantDisplayMode> argConstantDisplayMode
-	("smtlib-display-constants", llvm::cl::desc("Sets how bitvector constants are written in generated SMT-LIBv2 files (default=dec)"),
-	llvm::cl::values( clEnumValN(klee::ExprSMTLIBPrinter::BINARY, "bin","Use binary form (e.g. #b00101101)"),
-					  clEnumValN(klee::ExprSMTLIBPrinter::HEX, "hex","Use Hexadecimal form (e.g. #x2D)"),
-					  clEnumValN(klee::ExprSMTLIBPrinter::DECIMAL, "dec","Use decimal form (e.g. (_ bv45 8) )"),
-					  clEnumValEnd
-					),
-					llvm::cl::init(klee::ExprSMTLIBPrinter::DECIMAL)
+namespace ExprSMTLIBOptions {
+// Command line options
+llvm::cl::opt<klee::ExprSMTLIBPrinter::ConstantDisplayMode>
+argConstantDisplayMode(
+    "smtlib-display-constants",
+    llvm::cl::desc("Sets how bitvector constants are written in generated "
+                   "SMT-LIBv2 files (default=dec)"),
+    llvm::cl::values(clEnumValN(klee::ExprSMTLIBPrinter::BINARY, "bin",
+                                "Use binary form (e.g. #b00101101)"),
+                     clEnumValN(klee::ExprSMTLIBPrinter::HEX, "hex",
+                                "Use Hexadecimal form (e.g. #x2D)"),
+                     clEnumValN(klee::ExprSMTLIBPrinter::DECIMAL, "dec",
+                                "Use decimal form (e.g. (_ bv45 8) )"),
+                     clEnumValEnd),
+    llvm::cl::init(klee::ExprSMTLIBPrinter::DECIMAL));
+
+llvm::cl::opt<bool> humanReadableSMTLIB(
+    "smtlib-human-readable",
+    llvm::cl::desc(
+        "Enables generated SMT-LIBv2 files to be human readable (default=off)"),
+    llvm::cl::init(false));
+}
+
+namespace klee {
+
+ExprSMTLIBPrinter::ExprSMTLIBPrinter()
+    : usedArrays(), o(NULL), query(NULL), p(NULL), haveConstantArray(false),
+      logicToUse(QF_AUFBV),
+      humanReadable(ExprSMTLIBOptions::humanReadableSMTLIB),
+      smtlibBoolOptions(), arraysToCallGetValueOn(NULL) {
+  setConstantDisplayMode(ExprSMTLIBOptions::argConstantDisplayMode);
+}
+
+ExprSMTLIBPrinter::~ExprSMTLIBPrinter() {
+  if (p != NULL)
+    delete p;
+}
+
+void ExprSMTLIBPrinter::setOutput(std::ostream &output) {
+  o = &output;
+  if (p != NULL)
+    delete p;
+
+  p = new PrintContext(output);
+}
+
+void ExprSMTLIBPrinter::setQuery(const Query &q) {
+  query = &q;
+  reset(); // clear the data structures
+  scanAll();
+  negateQueryExpression();
+}
+
+void ExprSMTLIBPrinter::reset() {
+  usedArrays.clear();
+  haveConstantArray = false;
+
+  /* Clear the PRODUCE_MODELS option if it was automatically set.
+   * We need to do this because the next query might not need the
+   * (get-value) SMT-LIBv2 command.
+   */
+  if (arraysToCallGetValueOn != NULL)
+    setSMTLIBboolOption(PRODUCE_MODELS, OPTION_DEFAULT);
+
+  arraysToCallGetValueOn = NULL;
+}
+
+bool ExprSMTLIBPrinter::isHumanReadable() { return humanReadable; }
+
+bool ExprSMTLIBPrinter::setConstantDisplayMode(ConstantDisplayMode cdm) {
+  if (cdm > DECIMAL)
+    return false;
+
+  this->cdm = cdm;
+  return true;
+}
+
+void ExprSMTLIBPrinter::printConstant(const ref<ConstantExpr> &e) {
+  /* Handle simple boolean constants */
+
+  if (e->isTrue()) {
+    *p << "true";
+    return;
+  }
+
+  if (e->isFalse()) {
+    *p << "false";
+    return;
+  }
+
+  /* Handle bitvector constants */
+
+  std::string value;
+
+  /* SMTLIBv2 deduces the bit-width (should be 8-bits in our case)
+   * from the length of the string (e.g. zero is #b00000000). LLVM
+   * doesn't know about this so we need to pad the printed output
+   * with the appropriate number of zeros (zeroPad)
+   */
+  unsigned int zeroPad = 0;
+
+  switch (cdm) {
+  case BINARY:
+    e->toString(value, 2);
+    *p << "#b";
+
+    zeroPad = e->getWidth() - value.length();
+
+    for (unsigned int count = 0; count < zeroPad; count++)
+      *p << "0";
+
+    *p << value;
+    break;
+
+  case HEX:
+    e->toString(value, 16);
+    *p << "#x";
+
+    zeroPad = (e->getWidth() / 4) - value.length();
+    for (unsigned int count = 0; count < zeroPad; count++)
+      *p << "0";
+
+    *p << value;
+    break;
+
+  case DECIMAL:
+    e->toString(value, 10);
+    *p << "(_ bv" << value << " " << e->getWidth() << ")";
+    break;
+
+  default:
+    std::cerr << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant "
+                 "display mode" << std::endl;
+  }
+}
+
+void ExprSMTLIBPrinter::printExpression(
+    const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) {
+  // check if casting might be necessary
+  if (getSort(e) != expectedSort) {
+    printCastToSort(e, expectedSort);
+    return;
+  }
+
+  switch (e->getKind()) {
+  case Expr::Constant:
+    printConstant(cast<ConstantExpr>(e));
+    return; // base case
+
+  case Expr::NotOptimized:
+    // skip to child
+    printExpression(e->getKid(0), expectedSort);
+    return;
+
+  case Expr::Read:
+    printReadExpr(cast<ReadExpr>(e));
+    return;
+
+  case Expr::Extract:
+    printExtractExpr(cast<ExtractExpr>(e));
+    return;
+
+  case Expr::SExt:
+  case Expr::ZExt:
+    printCastExpr(cast<CastExpr>(e));
+    return;
+
+  case Expr::Ne:
+    printNotEqualExpr(cast<NeExpr>(e));
+    return;
+
+  case Expr::Select:
+    // the if-then-else expression.
+    printSelectExpr(cast<SelectExpr>(e), expectedSort);
+    return;
+
+  case Expr::Eq:
+    /* The "=" operator is special in that it can take any sort but we must
+     * enforce that both arguments are the same type. We do this a lazy way
+     * by enforcing the second argument is of the same type as the first.
+     */
+    printSortArgsExpr(e, getSort(e->getKid(0)));
+
+    return;
+
+  case Expr::And:
+  case Expr::Or:
+  case Expr::Xor:
+  case Expr::Not:
+    /* These operators have a bitvector version and a bool version.
+     * For these operators only (e.g. wouldn't apply to bvult) if the expected
+     * sort the
+     * expression is T then that implies the arguments are also of type T.
+     */
+    printLogicalOrBitVectorExpr(e, expectedSort);
+
+    return;
+
+  default:
+    /* The remaining operators (Add,Sub...,Ult,Ule,..)
+     * Expect SORT_BITVECTOR arguments
+     */
+    printSortArgsExpr(e, SORT_BITVECTOR);
+    return;
+  }
+}
+
+void ExprSMTLIBPrinter::printReadExpr(const ref<ReadExpr> &e) {
+  *p << "(" << getSMTLIBKeyword(e) << " ";
+  p->pushIndent();
+
+  printSeperator();
+
+  // print array with updates recursively
+  printUpdatesAndArray(e->updates.head, e->updates.root);
+
+  // print index
+  printSeperator();
+  printExpression(e->index, SORT_BITVECTOR);
+
+  p->popIndent();
+  printSeperator();
+  *p << ")";
+}
+
+void ExprSMTLIBPrinter::printExtractExpr(const ref<ExtractExpr> &e) {
+  unsigned int lowIndex = e->offset;
+  unsigned int highIndex = lowIndex + e->width - 1;
+
+  *p << "((_ " << getSMTLIBKeyword(e) << " " << highIndex << "  " << lowIndex
+     << ") ";
+
+  p->pushIndent(); // add indent for recursive call
+  printSeperator();
+
+  // recurse
+  printExpression(e->getKid(0), SORT_BITVECTOR);
+
+  p->popIndent(); // pop indent added for the recursive call
+  printSeperator();
+  *p << ")";
+}
+
+void ExprSMTLIBPrinter::printCastExpr(const ref<CastExpr> &e) {
+  /* sign_extend and zero_extend behave slightly unusually in SMTLIBv2
+   * instead of specifying of what bit-width we would like to extend to
+   * we specify how many bits to add to the child expression
+   *
+   * e.g
+   * ((_ sign_extend 64) (_ bv5 32))
+   *
+   * gives a (_ BitVec 96) instead of (_ BitVec 64)
+   *
+   * So we must work out how many bits we need to add.
+   *
+   * (e->width) is the desired number of bits
+   * (e->src->getWidth()) is the number of bits in the child
+   */
+  unsigned int numExtraBits = (e->width) - (e->src->getWidth());
+
+  *p << "((_ " << getSMTLIBKeyword(e) << " " << numExtraBits << ") ";
+
+  p->pushIndent(); // add indent for recursive call
+  printSeperator();
+
+  // recurse
+  printExpression(e->src, SORT_BITVECTOR);
+
+  p->popIndent(); // pop indent added for recursive call
+  printSeperator();
+
+  *p << ")";
+}
+
+void ExprSMTLIBPrinter::printNotEqualExpr(const ref<NeExpr> &e) {
+  *p << "(not (";
+  p->pushIndent();
+  *p << "="
+     << " ";
+  p->pushIndent();
+  printSeperator();
+
+  /* The "=" operators allows both sorts. We assume
+   * that the second argument sort should be forced to be the same sort as the
+   * first argument
+   */
+  SMTLIB_SORT s = getSort(e->getKid(0));
+
+  printExpression(e->getKid(0), s);
+  printSeperator();
+  printExpression(e->getKid(1), s);
+  p->popIndent();
+  printSeperator();
+
+  *p << ")";
+  p->popIndent();
+  printSeperator();
+  *p << ")";
+}
+
+const char *ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr> &e) {
+
+  switch (e->getKind()) {
+  case Expr::Read:
+    return "select";
+  case Expr::Select:
+    return "ite";
+  case Expr::Concat:
+    return "concat";
+  case Expr::Extract:
+    return "extract";
+  case Expr::ZExt:
+    return "zero_extend";
+  case Expr::SExt:
+    return "sign_extend";
+
+  case Expr::Add:
+    return "bvadd";
+  case Expr::Sub:
+    return "bvsub";
+  case Expr::Mul:
+    return "bvmul";
+  case Expr::UDiv:
+    return "bvudiv";
+  case Expr::SDiv:
+    return "bvsdiv";
+  case Expr::URem:
+    return "bvurem";
+  case Expr::SRem:
+    return "bvsrem";
+
+  /* And, Xor, Not and Or are not handled here because there different versions
+   * for different sorts. See printLogicalOrBitVectorExpr()
+   */
+
+  case Expr::Shl:
+    return "bvshl";
+  case Expr::LShr:
+    return "bvlshr";
+  case Expr::AShr:
+    return "bvashr";
+
+  case Expr::Eq:
+    return "=";
+
+  // Not Equal does not exist directly in SMTLIBv2
+
+  case Expr::Ult:
+    return "bvult";
+  case Expr::Ule:
+    return "bvule";
+  case Expr::Ugt:
+    return "bvugt";
+  case Expr::Uge:
+    return "bvuge";
+
+  case Expr::Slt:
+    return "bvslt";
+  case Expr::Sle:
+    return "bvsle";
+  case Expr::Sgt:
+    return "bvsgt";
+  case Expr::Sge:
+    return "bvsge";
+
+  default:
+    return "<error>";
+  }
+}
+
+void ExprSMTLIBPrinter::printUpdatesAndArray(const UpdateNode *un,
+                                             const Array *root) {
+  if (un != NULL) {
+    *p << "(store ";
+    p->pushIndent();
+    printSeperator();
+
+    // recurse to get the array or update that this store operations applies to
+    printUpdatesAndArray(un->next, root);
+
+    printSeperator();
+
+    // print index
+    printExpression(un->index, SORT_BITVECTOR);
+    printSeperator();
+
+    // print value that is assigned to this index of the array
+    printExpression(un->value, SORT_BITVECTOR);
+
+    p->popIndent();
+    printSeperator();
+    *p << ")";
+  } else {
+    // The base case of the recursion
+    *p << root->name;
+  }
+}
+
+void ExprSMTLIBPrinter::scanAll() {
+  // perform scan of all expressions
+  for (ConstraintManager::const_iterator i = query->constraints.begin();
+       i != query->constraints.end(); i++)
+    scan(*i);
+
+  // Scan the query too
+  scan(query->expr);
+}
+
+void ExprSMTLIBPrinter::generateOutput() {
+  if (p == NULL || query == NULL || o == NULL) {
+    std::cerr << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. "
+                 "Output or query bad!" << std::endl;
+    return;
+  }
+
+  if (humanReadable)
+    printNotice();
+  printOptions();
+  printSetLogic();
+  printArrayDeclarations();
+  printConstraints();
+  printQuery();
+  printAction();
+  printExit();
+}
+
+void ExprSMTLIBPrinter::printSetLogic() {
+  *o << "(set-logic ";
+  switch (logicToUse) {
+  case QF_ABV:
+    *o << "QF_ABV";
+    break;
+  case QF_AUFBV:
+    *o << "QF_AUFBV";
+    break;
+  }
+  *o << " )" << std::endl;
+}
+
+namespace {
+
+struct ArrayPtrsByName {
+  bool operator()(const Array *a1, const Array *a2) const {
+    return a1->name < a2->name;
+  }
+};
+
+}
+
+void ExprSMTLIBPrinter::printArrayDeclarations() {
+  // Assume scan() has been called
+  if (humanReadable)
+    *o << "; Array declarations" << endl;
+
+  // Declare arrays in a deterministic order.
+  std::vector<const Array *> sortedArrays(usedArrays.begin(), usedArrays.end());
+  std::sort(sortedArrays.begin(), sortedArrays.end(), ArrayPtrsByName());
+  for (std::vector<const Array *>::iterator it = sortedArrays.begin();
+       it != sortedArrays.end(); it++) {
+    *o << "(declare-fun " << (*it)->name << " () "
+                                            "(Array (_ BitVec "
+       << (*it)->getDomain() << ") "
+                                "(_ BitVec " << (*it)->getRange() << ") ) )"
+       << endl;
+  }
+
+  // Set array values for constant values
+  if (haveConstantArray) {
+    if (humanReadable)
+      *o << "; Constant Array Definitions" << endl;
+
+    const Array *array;
+
+    // loop over found arrays
+    for (std::vector<const Array *>::iterator it = sortedArrays.begin();
+         it != sortedArrays.end(); it++) {
+      array = *it;
+      int byteIndex = 0;
+      if (array->isConstantArray()) {
+        /*loop over elements in the array and generate an assert statement
+          for each one
+         */
+        for (vector<ref<ConstantExpr> >::const_iterator
+                 ce = array->constantValues.begin();
+             ce != array->constantValues.end(); ce++, byteIndex++) {
+          *p << "(assert (";
+          p->pushIndent();
+          *p << "= ";
+          p->pushIndent();
+          printSeperator();
+
+          *p << "(select " << array->name << " (_ bv" << byteIndex << " "
+             << array->getDomain() << ") )";
+          printSeperator();
+          printConstant((*ce));
+
+          p->popIndent();
+          printSeperator();
+          *p << ")";
+          p->popIndent();
+          printSeperator();
+          *p << ")";
+
+          p->breakLineI();
+        }
+      }
+    }
+  }
+}
+
+void ExprSMTLIBPrinter::printConstraints() {
+  if (humanReadable)
+    *o << "; Constraints" << endl;
+
+  // Generate assert statements for each constraint
+  for (ConstraintManager::const_iterator i = query->constraints.begin();
+       i != query->constraints.end(); i++) {
+    *p << "(assert ";
+    p->pushIndent();
+    printSeperator();
+
+    // recurse into Expression
+    printExpression(*i, SORT_BOOL);
+
+    p->popIndent();
+    printSeperator();
+    *p << ")";
+    p->breakLineI();
+  }
+}
+
+void ExprSMTLIBPrinter::printAction() {
+  // Ask solver to check for satisfiability
+  *o << "(check-sat)" << endl;
+
+  /* If we has arrays to find the values of then we'll
+   * ask the solver for the value of each bitvector in each array
+   */
+  if (arraysToCallGetValueOn != NULL && !arraysToCallGetValueOn->empty()) {
+
+    const Array *theArray = 0;
+
+    // loop over the array names
+    for (vector<const Array *>::const_iterator it =
+             arraysToCallGetValueOn->begin();
+         it != arraysToCallGetValueOn->end(); it++) {
+      theArray = *it;
+      // Loop over the array indices
+      for (unsigned int index = 0; index < theArray->size; ++index) {
+        *o << "(get-value ( (select " << (**it).name << " (_ bv" << index << " "
+           << theArray->getDomain() << ") ) ) )" << endl;
+      }
+    }
+  }
+}
+
+void ExprSMTLIBPrinter::scan(const ref<Expr> &e) {
+  if (e.isNull()) {
+    std::cerr << "ExprSMTLIBPrinter::scan() : Found NULL expression!"
+              << std::endl;
+    return;
+  }
+
+  if (isa<ConstantExpr>(e))
+    return; // we don't need to scan simple constants
+
+  if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
 
+    // Attempt to insert array and if array wasn't present before do more things
+    if (usedArrays.insert(re->updates.root).second) {
 
-	);
+      // check if the array is constant
+      if (re->updates.root->isConstantArray())
+        haveConstantArray = true;
+
+      // scan the update list
+      scanUpdates(re->updates.head);
+    }
+  }
+
+  // recurse into the children
+  Expr *ep = e.get();
+  for (unsigned int i = 0; i < ep->getNumKids(); i++)
+    scan(ep->getKid(i));
+}
+
+void ExprSMTLIBPrinter::scanUpdates(const UpdateNode *un) {
+  while (un != NULL) {
+    scan(un->index);
+    scan(un->value);
+    un = un->next;
+  }
+}
+
+void ExprSMTLIBPrinter::printExit() { *o << "(exit)" << endl; }
+
+bool ExprSMTLIBPrinter::setLogic(SMTLIBv2Logic l) {
+  if (l > QF_AUFBV)
+    return false;
+
+  logicToUse = l;
+  return true;
+}
 
-	llvm::cl::opt<bool> humanReadableSMTLIB("smtlib-human-readable",
-				llvm::cl::desc("Enables generated SMT-LIBv2 files to be human readable (default=off)"),
-				llvm::cl::init(false)
+void ExprSMTLIBPrinter::printSeperator() {
+  if (humanReadable)
+    p->breakLineI();
+  else
+    p->write(" ");
+}
 
+void ExprSMTLIBPrinter::printNotice() {
+  *o << "; This file conforms to SMTLIBv2 and was generated by KLEE" << endl;
+}
 
-	);
+void ExprSMTLIBPrinter::setHumanReadable(bool hr) { humanReadable = hr; }
 
+void ExprSMTLIBPrinter::printOptions() {
+  // Print out SMTLIBv2 boolean options
+  for (std::map<SMTLIBboolOptions, bool>::const_iterator i =
+           smtlibBoolOptions.begin();
+       i != smtlibBoolOptions.end(); i++) {
+    *o << "(set-option :" << getSMTLIBOptionString(i->first) << " "
+       << ((i->second) ? "true" : "false") << ")" << endl;
+  }
 }
 
+void ExprSMTLIBPrinter::printQuery() {
+  if (humanReadable) {
+    *p << "; Query from solver turned into an assert";
+    p->breakLineI();
+  }
 
-namespace klee
-{
+  p->pushIndent();
+  *p << "(assert";
+  p->pushIndent();
+  printSeperator();
 
-	ExprSMTLIBPrinter::ExprSMTLIBPrinter() :
-		usedArrays(), o(NULL), query(NULL), p(NULL), haveConstantArray(false), logicToUse(QF_AUFBV),
-		humanReadable(ExprSMTLIBOptions::humanReadableSMTLIB), smtlibBoolOptions(), arraysToCallGetValueOn(NULL)
-	{
-		setConstantDisplayMode(ExprSMTLIBOptions::argConstantDisplayMode);
-	}
+  printExpression(queryAssert, SORT_BOOL);
 
-	ExprSMTLIBPrinter::~ExprSMTLIBPrinter()
-	{
-		if(p!=NULL)
-			delete p;
-	}
+  p->popIndent();
+  printSeperator();
+  *p << ")";
+  p->popIndent();
+  p->breakLineI();
+}
 
-	void ExprSMTLIBPrinter::setOutput(std::ostream& output)
-	{
-		o = &output;
-		if(p!=NULL)
-			delete p;
+ExprSMTLIBPrinter::SMTLIB_SORT ExprSMTLIBPrinter::getSort(const ref<Expr> &e) {
+  /* We could handle every operator in a large switch statement,
+   * but this seems more elegant.
+   */
+
+  if (e->getKind() == Expr::Extract) {
+    /* This is a special corner case. In most cases if a node in the expression
+     * tree
+     * is of width 1 it should be considered as SORT_BOOL. However it is
+     * possible to
+     * perform an extract operation on a SORT_BITVECTOR and produce a
+     * SORT_BITVECTOR of length 1.
+     * The ((_ extract i j) () ) operation in SMTLIBv2 always produces
+     * SORT_BITVECTOR
+     */
+    return SORT_BITVECTOR;
+  } else
+    return (e->getWidth() == Expr::Bool) ? (SORT_BOOL) : (SORT_BITVECTOR);
+}
 
-		p = new PrintContext(output);
-	}
+void ExprSMTLIBPrinter::printCastToSort(const ref<Expr> &e,
+                                        ExprSMTLIBPrinter::SMTLIB_SORT sort) {
+  switch (sort) {
+  case SORT_BITVECTOR:
+    if (humanReadable) {
+      p->breakLineI();
+      *p << ";Performing implicit bool to bitvector cast";
+      p->breakLine();
+    }
+    // We assume the e is a bool that we need to cast to a bitvector sort.
+    *p << "(ite";
+    p->pushIndent();
+    printSeperator();
+    printExpression(e, SORT_BOOL);
+    printSeperator();
+    *p << "(_ bv1 1)";
+    printSeperator(); // printing the "true" bitvector
+    *p << "(_ bv0 1)";
+    p->popIndent();
+    printSeperator(); // printing the "false" bitvector
+    *p << ")";
+    break;
+  case SORT_BOOL: {
+    /* We make the assumption (might be wrong) that any bitvector whos unsigned
+     *decimal value is
+     * is zero is interpreted as "false", otherwise it is true.
+     *
+     * This may not be the interpretation we actually want!
+     */
+    Expr::Width bitWidth = e->getWidth();
+    if (humanReadable) {
+      p->breakLineI();
+      *p << ";Performing implicit bitvector to bool cast";
+      p->breakLine();
+    }
+    *p << "(bvugt";
+    p->pushIndent();
+    printSeperator();
+    // We assume is e is a bitvector
+    printExpression(e, SORT_BITVECTOR);
+    printSeperator();
+    *p << "(_ bv0 " << bitWidth << ")";
+    p->popIndent();
+    printSeperator(); // Zero bitvector of required width
+    *p << ")";
+
+    if (bitWidth != Expr::Bool)
+      std::cerr << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length "
+                << bitWidth << ") to bool!" << std::endl;
+
+  } break;
+  default:
+    assert(0 && "Unsupported cast!");
+  }
+}
+
+void ExprSMTLIBPrinter::printSelectExpr(const ref<SelectExpr> &e,
+                                        ExprSMTLIBPrinter::SMTLIB_SORT s) {
+  // This is the if-then-else expression
 
-	void ExprSMTLIBPrinter::setQuery(const Query& q)
-	{
-		query = &q;
-		reset(); // clear the data structures
-		scanAll();
-		negateQueryExpression();
-	}
+  *p << "(" << getSMTLIBKeyword(e) << " ";
+  p->pushIndent(); // add indent for recursive call
 
-	void ExprSMTLIBPrinter::reset()
-	{
-		usedArrays.clear();
-		haveConstantArray=false;
+  // The condition
+  printSeperator();
+  printExpression(e->getKid(0), SORT_BOOL);
 
-		/* Clear the PRODUCE_MODELS option if it was automatically set.
-		 * We need to do this because the next query might not need the
-		 * (get-value) SMT-LIBv2 command.
-		 */
-		if(arraysToCallGetValueOn !=NULL)
-			setSMTLIBboolOption(PRODUCE_MODELS,OPTION_DEFAULT);
+  /* This operator is special in that the remaining children
+   * can be of any sort.
+   */
 
-		arraysToCallGetValueOn=NULL;
+  // if true
+  printSeperator();
+  printExpression(e->getKid(1), s);
 
+  // if false
+  printSeperator();
+  printExpression(e->getKid(2), s);
 
-	}
-
-	bool ExprSMTLIBPrinter::isHumanReadable()
-	{
-		return humanReadable;
-	}
+  p->popIndent(); // pop indent added for recursive call
+  printSeperator();
+  *p << ")";
+}
 
-	bool ExprSMTLIBPrinter::setConstantDisplayMode(ConstantDisplayMode cdm)
-	{
-		if(cdm > DECIMAL)
-			return false;
+void ExprSMTLIBPrinter::printSortArgsExpr(const ref<Expr> &e,
+                                          ExprSMTLIBPrinter::SMTLIB_SORT s) {
+  *p << "(" << getSMTLIBKeyword(e) << " ";
+  p->pushIndent(); // add indent for recursive call
 
-		this->cdm = cdm;
-		return true;
-	}
+  // loop over children and recurse into each expecting they are of sort "s"
+  for (unsigned int i = 0; i < e->getNumKids(); i++) {
+    printSeperator();
+    printExpression(e->getKid(i), s);
+  }
 
-	void ExprSMTLIBPrinter::printConstant(const ref<ConstantExpr>& e)
-	{
-		/* Handle simple boolean constants */
-
-		if(e->isTrue())
-		{
-			*p << "true";
-			return;
-		}
-
-		if(e->isFalse())
-		{
-			*p << "false";
-			return;
-		}
-
-		/* Handle bitvector constants */
-
-		std::string value;
-
-		/* SMTLIBv2 deduces the bit-width (should be 8-bits in our case)
-		 * from the length of the string (e.g. zero is #b00000000). LLVM
-		 * doesn't know about this so we need to pad the printed output
-		 * with the appropriate number of zeros (zeroPad)
-		 */
-		unsigned int zeroPad=0;
-
-		switch(cdm)
-		{
-			case BINARY:
-				e->toString(value,2);
-				*p << "#b";
-
-				zeroPad = e->getWidth() - value.length();
-
-				for(unsigned int count=0; count < zeroPad; count++)
-					*p << "0";
-
-				*p << value ;
-				break;
-
-			case HEX:
-				e->toString(value,16);
-				*p << "#x";
-
-				zeroPad =  (e->getWidth() / 4) - value.length();
-				for(unsigned int count=0; count < zeroPad; count++)
-					*p << "0";
-
-				*p << value ;
-				break;
-
-			case DECIMAL:
-				e->toString(value,10);
-				*p << "(_ bv" << value<< " " << e->getWidth() << ")";
-				break;
-
-			default:
-				std::cerr << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant display mode" << std::endl;
-		}
-	}
-
-	void ExprSMTLIBPrinter::printExpression(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort)
-	{
-		//check if casting might be necessary
-		if(getSort(e) != expectedSort)
-		{
-			printCastToSort(e,expectedSort);
-			return;
-		}
-
-
-		switch(e->getKind())
-		{
-			case Expr::Constant:
-				printConstant(cast<ConstantExpr>(e));
-				return; //base case
-
-			case Expr::NotOptimized:
-				//skip to child
-				printExpression(e->getKid(0),expectedSort);
-				return;
-
-			case Expr::Read:
-				printReadExpr(cast<ReadExpr>(e));
-				return;
-
-			case Expr::Extract:
-				printExtractExpr(cast<ExtractExpr>(e));
-				return;
-
-			case Expr::SExt:
-			case Expr::ZExt:
-				printCastExpr(cast<CastExpr>(e));
-				return;
-
-			case Expr::Ne:
-				printNotEqualExpr(cast<NeExpr>(e));
-				return;
-
-			case Expr::Select:
-				//the if-then-else expression.
-				printSelectExpr(cast<SelectExpr>(e),expectedSort);
-				return;
-
-			case Expr::Eq:
-				/* The "=" operator is special in that it can take any sort but we must
-				 * enforce that both arguments are the same type. We do this a lazy way
-				 * by enforcing the second argument is of the same type as the first.
-				 */
-				printSortArgsExpr(e,getSort(e->getKid(0)));
-
-				return;
-
-			case Expr::And:
-			case Expr::Or:
-			case Expr::Xor:
-			case Expr::Not:
-				/* These operators have a bitvector version and a bool version.
-				 * For these operators only (e.g. wouldn't apply to bvult) if the expected sort the
-				 * expression is T then that implies the arguments are also of type T.
-				 */
-				printLogicalOrBitVectorExpr(e,expectedSort);
-
-				return;
-
-
-			default:
-				/* The remaining operators (Add,Sub...,Ult,Ule,..)
-				 * Expect SORT_BITVECTOR arguments
-				 */
-				printSortArgsExpr(e,SORT_BITVECTOR);
-				return;
-		}
-	}
-
-	void ExprSMTLIBPrinter::printReadExpr(const ref<ReadExpr>& e)
-	{
-		*p << "(" << getSMTLIBKeyword(e) << " ";
-		p->pushIndent();
-
-		printSeperator();
-
-		//print array with updates recursively
-		printUpdatesAndArray(e->updates.head,e->updates.root);
-
-		//print index
-		printSeperator();
-		printExpression(e->index,SORT_BITVECTOR);
-
-		p->popIndent();
-		printSeperator();
-		*p << ")";
-	}
-
-	void ExprSMTLIBPrinter::printExtractExpr(const ref<ExtractExpr>& e)
-	{
-		unsigned int lowIndex= e->offset;
-		unsigned int highIndex= lowIndex + e->width -1;
-
-		*p << "((_ " << getSMTLIBKeyword(e) << " " << highIndex << "  " << lowIndex << ") ";
-
-		p->pushIndent(); //add indent for recursive call
-		printSeperator();
-
-		//recurse
-		printExpression(e->getKid(0),SORT_BITVECTOR);
-
-		p->popIndent(); //pop indent added for the recursive call
-		printSeperator();
-		*p << ")";
-	}
-
-	void ExprSMTLIBPrinter::printCastExpr(const ref<CastExpr>& e)
-	{
-		/* sign_extend and zero_extend behave slightly unusually in SMTLIBv2
-		 * instead of specifying of what bit-width we would like to extend to
-		 * we specify how many bits to add to the child expression
-		 *
-		 * e.g
-		 * ((_ sign_extend 64) (_ bv5 32))
-		 *
-		 * gives a (_ BitVec 96) instead of (_ BitVec 64)
-		 *
-		 * So we must work out how many bits we need to add.
-		 *
-		 * (e->width) is the desired number of bits
-		 * (e->src->getWidth()) is the number of bits in the child
-		 */
-		unsigned int numExtraBits= (e->width) - (e->src->getWidth());
-
-		*p << "((_ " << getSMTLIBKeyword(e) << " " <<
-				numExtraBits << ") ";
-
-		p->pushIndent(); //add indent for recursive call
-		printSeperator();
-
-		//recurse
-		printExpression(e->src,SORT_BITVECTOR);
-
-		p->popIndent(); //pop indent added for recursive call
-		printSeperator();
-
-		*p << ")";
-	}
-
-	void ExprSMTLIBPrinter::printNotEqualExpr(const ref<NeExpr>& e)
-	{
-		*p << "(not (";
-		p->pushIndent();
-		*p << "=" << " ";
-		p->pushIndent();
-		printSeperator();
-
-		/* The "=" operators allows both sorts. We assume
-		 * that the second argument sort should be forced to be the same sort as the
-		 * first argument
-		 */
-		SMTLIB_SORT s = getSort(e->getKid(0));
-
-		printExpression(e->getKid(0),s);
-		printSeperator();
-		printExpression(e->getKid(1),s);
-		p->popIndent();
-		printSeperator();
-
-		*p << ")";
-		p->popIndent();
-		printSeperator();
-		*p << ")";
-	}
-
-
-	const char* ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr>& e)
-	{
-
-		switch(e->getKind())
-		{
-			case Expr::Read: return "select";
-			case Expr::Select: return "ite";
-			case Expr::Concat: return "concat";
-			case Expr::Extract: return "extract";
-			case Expr::ZExt: return "zero_extend";
-			case Expr::SExt: return "sign_extend";
-
-			case Expr::Add: return "bvadd";
-			case Expr::Sub: return "bvsub";
-			case Expr::Mul: return "bvmul";
-			case Expr::UDiv: return "bvudiv";
-			case Expr::SDiv: return "bvsdiv";
-			case Expr::URem: return "bvurem";
-			case Expr::SRem: return "bvsrem";
-
-
-			/* And, Xor, Not and Or are not handled here because there different versions
-			 * for different sorts. See printLogicalOrBitVectorExpr()
-			 */
-
-
-			case Expr::Shl: return "bvshl";
-			case Expr::LShr: return "bvlshr";
-			case Expr::AShr: return "bvashr";
-
-			case Expr::Eq: return "=";
-
-			//Not Equal does not exist directly in SMTLIBv2
-
-			case Expr::Ult: return "bvult";
-			case Expr::Ule: return "bvule";
-			case Expr::Ugt: return "bvugt";
-			case Expr::Uge: return "bvuge";
-
-			case Expr::Slt: return "bvslt";
-			case Expr::Sle: return "bvsle";
-			case Expr::Sgt: return "bvsgt";
-			case Expr::Sge: return "bvsge";
-
-			default:
-				return "<error>";
-
-		}
-	}
-
-	void ExprSMTLIBPrinter::printUpdatesAndArray(const UpdateNode* un, const Array* root)
-	{
-		if(un!=NULL)
-		{
-			*p << "(store ";
-			p->pushIndent();
-			printSeperator();
-
-			//recurse to get the array or update that this store operations applies to
-			printUpdatesAndArray(un->next,root);
-
-			printSeperator();
-
-			//print index
-			printExpression(un->index,SORT_BITVECTOR);
-			printSeperator();
-
-			//print value that is assigned to this index of the array
-			printExpression(un->value,SORT_BITVECTOR);
-
-			p->popIndent();
-			printSeperator();
-			*p << ")";
-		}
-		else
-		{
-			//The base case of the recursion
-			*p << root->name;
-		}
-
-	}
-
-	void ExprSMTLIBPrinter::scanAll()
-	{
-		//perform scan of all expressions
-		for(ConstraintManager::const_iterator i= query->constraints.begin(); i != query->constraints.end(); i++)
-			scan(*i);
-
-		//Scan the query too
-		scan(query->expr);
-	}
-
-	void ExprSMTLIBPrinter::generateOutput()
-	{
-		if(p==NULL || query == NULL || o ==NULL)
-		{
-			std::cerr << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. Output or query bad!" << std::endl;
-			return;
-		}
-
-		if(humanReadable) printNotice();
-		printOptions();
-		printSetLogic();
-		printArrayDeclarations();
-		printConstraints();
-		printQuery();
-		printAction();
-		printExit();
-	}
-
-	void ExprSMTLIBPrinter::printSetLogic()
-	{
-		*o << "(set-logic ";
-		switch(logicToUse)
-		{
-		case QF_ABV: *o << "QF_ABV"; break;
-		case QF_AUFBV: *o << "QF_AUFBV" ; break;
-		}
-		*o << " )" << std::endl;
-	}
-
-
-	void ExprSMTLIBPrinter::printArrayDeclarations()
-	{
-		//Assume scan() has been called
-		if(humanReadable)
-			*o << "; Array declarations" << endl;
-
-		//declare arrays
-		for(set<const Array*>::iterator it = usedArrays.begin(); it != usedArrays.end(); it++)
-		{
-			*o << "(declare-fun " << (*it)->name << " () "
-				 "(Array (_ BitVec " << (*it)->getDomain() << ") "
-				 "(_ BitVec " << (*it)->getRange() << ") ) )" << endl;
-		}
-
-		//Set array values for constant values
-		if(haveConstantArray)
-		{
-			if(humanReadable)
-				*o << "; Constant Array Definitions" << endl;
-
-			const Array* array;
-
-			//loop over found arrays
-			for(set<const Array*>::iterator it = usedArrays.begin(); it != usedArrays.end(); it++)
-			{
-				array= *it;
-				int byteIndex=0;
-				if(array->isConstantArray())
-				{
-					/*loop over elements in the array and generate an assert statement
-					  for each one
-					 */
-					for(vector< ref<ConstantExpr> >::const_iterator ce= array->constantValues.begin();
-							ce != array->constantValues.end(); ce++, byteIndex++)
-					{
-						*p << "(assert (";
-						p->pushIndent();
-						*p <<           "= ";
-						p->pushIndent();
-						printSeperator();
-
-						*p << "(select " << array->name << " (_ bv" << byteIndex << " " << array->getDomain() << ") )";
-						printSeperator();
-						printConstant((*ce));
-
-						p->popIndent();
-						printSeperator();
-						*p << ")";
-						p->popIndent();
-						printSeperator();
-						*p << ")";
-
-						p->breakLineI();
-
-					}
-				}
-			}
-		}
-	}
-
-	void ExprSMTLIBPrinter::printConstraints()
-	{
-		if(humanReadable)
-			*o << "; Constraints" << endl;
-
-		//Generate assert statements for each constraint
-		for(ConstraintManager::const_iterator i= query->constraints.begin(); i != query->constraints.end(); i++)
-		{
-			*p << "(assert ";
-			p->pushIndent();
-			printSeperator();
-
-			//recurse into Expression
-			printExpression(*i,SORT_BOOL);
-
-			p->popIndent();
-			printSeperator();
-			*p << ")"; p->breakLineI();
-		}
-
-	}
-
-	void ExprSMTLIBPrinter::printAction()
-	{
-		//Ask solver to check for satisfiability
-		*o << "(check-sat)" << endl;
-
-		/* If we has arrays to find the values of then we'll
-		 * ask the solver for the value of each bitvector in each array
-		 */
-		if(arraysToCallGetValueOn!=NULL && !arraysToCallGetValueOn->empty())
-		{
-
-			const Array* theArray=0;
-
-			//loop over the array names
-			for(vector<const Array*>::const_iterator it = arraysToCallGetValueOn->begin(); it != arraysToCallGetValueOn->end(); it++)
-			{
-				theArray=*it;
-				//Loop over the array indices
-				for(unsigned int index=0; index < theArray->size; ++index)
-				{
-					*o << "(get-value ( (select " << (**it).name <<
-					     " (_ bv" << index << " " << theArray->getDomain() << ") ) ) )" << endl;
-				}
-
-			}
-
-
-		}
-	}
-
-	void ExprSMTLIBPrinter::scan(const ref<Expr>& e)
-	{
-		if(e.isNull())
-		{
-			std::cerr << "ExprSMTLIBPrinter::scan() : Found NULL expression!" << std::endl;
-			return;
-		}
-
-		if(isa<ConstantExpr>(e))
-			return; //we don't need to scan simple constants
-
-		if(const ReadExpr* re = dyn_cast<ReadExpr>(e))
-		{
-
-			//Attempt to insert array and if array wasn't present before do more things
-			if(usedArrays.insert(re->updates.root).second)
-			{
-
-				//check if the array is constant
-				if( re->updates.root->isConstantArray())
-					haveConstantArray=true;
-
-				//scan the update list
-				scanUpdates(re->updates.head);
-
-			}
-
-		}
-
-		//recurse into the children
-		Expr* ep = e.get();
-		for(unsigned int i=0; i < ep->getNumKids(); i++)
-			scan(ep->getKid(i));
-	}
-
-
-	void ExprSMTLIBPrinter::scanUpdates(const UpdateNode* un)
-	{
-		while(un != NULL)
-		{
-			scan(un->index);
-			scan(un->value);
-			un= un->next;
-		}
-	}
-
-
-	void ExprSMTLIBPrinter::printExit()
-	{
-		*o << "(exit)" << endl;
-	}
-
-	bool ExprSMTLIBPrinter::setLogic(SMTLIBv2Logic l)
-	{
-		if(l > QF_AUFBV)
-			return false;
-
-		logicToUse=l;
-		return true;
-	}
-
-	void ExprSMTLIBPrinter::printSeperator()
-	{
-		if(humanReadable)
-			p->breakLineI();
-		else
-			p->write(" ");
-	}
-
-	void ExprSMTLIBPrinter::printNotice()
-	{
-		*o << "; This file conforms to SMTLIBv2 and was generated by KLEE" << endl;
-	}
-
-	void ExprSMTLIBPrinter::setHumanReadable(bool hr)
-	{
-		humanReadable=hr;
-	}
-
-	void ExprSMTLIBPrinter::printOptions()
-	{
-		//Print out SMTLIBv2 boolean options
-		for(std::map<SMTLIBboolOptions,bool>::const_iterator i= smtlibBoolOptions.begin(); i!= smtlibBoolOptions.end(); i++)
-		{
-			*o << "(set-option :" << getSMTLIBOptionString(i->first) <<
-			" " << ((i->second)?"true":"false") << ")" << endl;
-		}
-	}
-
-	void ExprSMTLIBPrinter::printQuery()
-	{
-		if(humanReadable)
-		{
-			*p << "; Query from solver turned into an assert";
-			p->breakLineI();
-		}
-
-		p->pushIndent();
-		*p << "(assert";
-		p->pushIndent();
-		printSeperator();
-
-		printExpression(queryAssert,SORT_BOOL);
-
-		p->popIndent();
-		printSeperator();
-		*p << ")";
-		p->popIndent();
-		p->breakLineI();
-	}
-
-	ExprSMTLIBPrinter::SMTLIB_SORT ExprSMTLIBPrinter::getSort(const ref<Expr>& e)
-	{
-		/* We could handle every operator in a large switch statement,
-		 * but this seems more elegant.
-		 */
-
-		if(e->getKind() == Expr::Extract)
-		{
-			/* This is a special corner case. In most cases if a node in the expression tree
-			 * is of width 1 it should be considered as SORT_BOOL. However it is possible to
-			 * perform an extract operation on a SORT_BITVECTOR and produce a SORT_BITVECTOR of length 1.
-			 * The ((_ extract i j) () ) operation in SMTLIBv2 always produces SORT_BITVECTOR
-			 */
-			return SORT_BITVECTOR;
-		}
-		else
-			return (e->getWidth() == Expr::Bool)?(SORT_BOOL):(SORT_BITVECTOR);
-	}
-
-	void ExprSMTLIBPrinter::printCastToSort(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT sort)
-	{
-		switch(sort)
-		{
-			case SORT_BITVECTOR:
-				if(humanReadable)
-				{
-					p->breakLineI(); *p << ";Performing implicit bool to bitvector cast"; p->breakLine();
-				}
-				//We assume the e is a bool that we need to cast to a bitvector sort.
-				*p << "(ite"; p->pushIndent(); printSeperator();
-				printExpression(e,SORT_BOOL); printSeperator();
-				*p << "(_ bv1 1)" ; printSeperator(); //printing the "true" bitvector
-				*p << "(_ bv0 1)" ; p->popIndent(); printSeperator(); //printing the "false" bitvector
-				*p << ")";
-				break;
-			case SORT_BOOL:
-			{
-				/* We make the assumption (might be wrong) that any bitvector whos unsigned decimal value is
-				 * is zero is interpreted as "false", otherwise it is true.
-				 *
-				 * This may not be the interpretation we actually want!
-				 */
-				Expr::Width bitWidth=e->getWidth();
-				if(humanReadable)
-				{
-					p->breakLineI(); *p << ";Performing implicit bitvector to bool cast"; p->breakLine();
-				}
-				*p << "(bvugt"; p->pushIndent(); printSeperator();
-				// We assume is e is a bitvector
-				printExpression(e,SORT_BITVECTOR); printSeperator();
-				*p << "(_ bv0 " << bitWidth << ")"; p->popIndent(); printSeperator(); //Zero bitvector of required width
-				*p << ")";
-
-				if(bitWidth!=Expr::Bool)
-					std::cerr << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length " << bitWidth << ") to bool!" << std::endl;
-
-			}
-				break;
-			default:
-				assert(0 && "Unsupported cast!");
-		}
-	}
-
-	void ExprSMTLIBPrinter::printSelectExpr(const ref<SelectExpr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s)
-	{
-		//This is the if-then-else expression
-
-		*p << "(" << getSMTLIBKeyword(e) << " ";
-		p->pushIndent(); //add indent for recursive call
-
-			//The condition
-			printSeperator();
-			printExpression(e->getKid(0),SORT_BOOL);
-
-			/* This operator is special in that the remaining children
-			 * can be of any sort.
-			 */
-
-			//if true
-			printSeperator();
-			printExpression(e->getKid(1),s);
-
-			//if false
-			printSeperator();
-			printExpression(e->getKid(2),s);
-
-
-		p->popIndent(); //pop indent added for recursive call
-		printSeperator();
-		*p << ")";
-	}
-
-	void ExprSMTLIBPrinter::printSortArgsExpr(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s)
-	{
-		*p << "(" << getSMTLIBKeyword(e) << " ";
-		p->pushIndent(); //add indent for recursive call
-
-		//loop over children and recurse into each expecting they are of sort "s"
-		for(unsigned int i=0; i < e->getNumKids(); i++)
-		{
-			printSeperator();
-			printExpression(e->getKid(i),s);
-		}
-
-		p->popIndent(); //pop indent added for recursive call
-		printSeperator();
-		*p << ")";
-	}
-
-	void ExprSMTLIBPrinter::printLogicalOrBitVectorExpr(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s)
-	{
-		/* For these operators it is the case that the expected sort is the same as the sorts
-		 * of the arguments.
-		 */
-
-		*p << "(";
-		switch(e->getKind())
-		{
-			case Expr::And:
-				*p << ((s==SORT_BITVECTOR)?"bvand":"and");
-				break;
-			case Expr::Not:
-				*p << ((s==SORT_BITVECTOR)?"bvnot":"not");
-				break;
-			case Expr::Or:
-				*p << ((s==SORT_BITVECTOR)?"bvor":"or");
-				break;
-
-			case Expr::Xor:
-				*p << ((s==SORT_BITVECTOR)?"bvxor":"xor");
-				break;
-			default:
-				*p << "ERROR"; // this shouldn't happen
-		}
-		*p << " ";
-
-		p->pushIndent(); //add indent for recursive call
-
-		//loop over children and recurse into each expecting they are of sort "s"
-		for(unsigned int i=0; i < e->getNumKids(); i++)
-		{
-			printSeperator();
-			printExpression(e->getKid(i),s);
-		}
-
-		p->popIndent(); //pop indent added for recursive call
-		printSeperator();
-		*p << ")";
-	}
-
-	void ExprSMTLIBPrinter::negateQueryExpression()
-	{
-		//Negating the query
-		queryAssert = Expr::createIsZero(query->expr);
-	}
-
-	bool ExprSMTLIBPrinter::setSMTLIBboolOption(SMTLIBboolOptions option, SMTLIBboolValues value)
-	{
-		std::pair< std::map<SMTLIBboolOptions,bool>::iterator, bool> thePair;
-		bool theValue=  (value==OPTION_TRUE)?true:false;
-
-		switch(option)
-		{
-			case PRINT_SUCCESS:
-			case PRODUCE_MODELS:
-			case INTERACTIVE_MODE:
-				thePair=smtlibBoolOptions.insert(std::pair<SMTLIBboolOptions,bool>(option,theValue));
-
-				if(value== OPTION_DEFAULT)
-				{
-					//we should unset (by removing from map) this option so the solver uses its default
-					smtlibBoolOptions.erase(thePair.first);
-					return true;
-				}
-
-				if(!thePair.second)
-				{
-					//option was already present so modify instead.
-					thePair.first->second=value;
-				}
-				return true;
-			default:
-				return false;
-
-		}
-	}
-
-	void ExprSMTLIBPrinter::setArrayValuesToGet(const std::vector<const Array*>& a)
-	{
-		arraysToCallGetValueOn = &a;
-
-		//This option must be set in order to use the SMTLIBv2 command (get-value () )
-		if(!a.empty())
-			setSMTLIBboolOption(PRODUCE_MODELS,OPTION_TRUE);
-
-		/* There is a risk that users will ask about array values that aren't
-		 * even in the query. We should add them to the usedArrays list and hope
-		 * that the solver knows what to do when we ask for the values of arrays
-		 * that don't feature in our query!
-		 */
-		for(vector<const Array*>::const_iterator i = a.begin(); i!= a.end() ; ++i)
-		{
-			usedArrays.insert(*i);
-		}
-
-	}
-
-const char* ExprSMTLIBPrinter::getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option)
-{
-	switch(option)
-	{
-		case PRINT_SUCCESS: return "print-success";
-		case PRODUCE_MODELS: return "produce-models";
-		case INTERACTIVE_MODE: return "interactive-mode";
-		default:
-			return "unknown-option";
-	}
+  p->popIndent(); // pop indent added for recursive call
+  printSeperator();
+  *p << ")";
 }
 
+void ExprSMTLIBPrinter::printLogicalOrBitVectorExpr(
+    const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT s) {
+  /* For these operators it is the case that the expected sort is the same as
+   * the sorts
+   * of the arguments.
+   */
+
+  *p << "(";
+  switch (e->getKind()) {
+  case Expr::And:
+    *p << ((s == SORT_BITVECTOR) ? "bvand" : "and");
+    break;
+  case Expr::Not:
+    *p << ((s == SORT_BITVECTOR) ? "bvnot" : "not");
+    break;
+  case Expr::Or:
+    *p << ((s == SORT_BITVECTOR) ? "bvor" : "or");
+    break;
+
+  case Expr::Xor:
+    *p << ((s == SORT_BITVECTOR) ? "bvxor" : "xor");
+    break;
+  default:
+    *p << "ERROR"; // this shouldn't happen
+  }
+  *p << " ";
+
+  p->pushIndent(); // add indent for recursive call
+
+  // loop over children and recurse into each expecting they are of sort "s"
+  for (unsigned int i = 0; i < e->getNumKids(); i++) {
+    printSeperator();
+    printExpression(e->getKid(i), s);
+  }
+
+  p->popIndent(); // pop indent added for recursive call
+  printSeperator();
+  *p << ")";
 }
 
+void ExprSMTLIBPrinter::negateQueryExpression() {
+  // Negating the query
+  queryAssert = Expr::createIsZero(query->expr);
+}
+
+bool ExprSMTLIBPrinter::setSMTLIBboolOption(SMTLIBboolOptions option,
+                                            SMTLIBboolValues value) {
+  std::pair<std::map<SMTLIBboolOptions, bool>::iterator, bool> thePair;
+  bool theValue = (value == OPTION_TRUE) ? true : false;
+
+  switch (option) {
+  case PRINT_SUCCESS:
+  case PRODUCE_MODELS:
+  case INTERACTIVE_MODE:
+    thePair = smtlibBoolOptions.insert(
+        std::pair<SMTLIBboolOptions, bool>(option, theValue));
+
+    if (value == OPTION_DEFAULT) {
+      // we should unset (by removing from map) this option so the solver uses
+      // its default
+      smtlibBoolOptions.erase(thePair.first);
+      return true;
+    }
+
+    if (!thePair.second) {
+      // option was already present so modify instead.
+      thePair.first->second = value;
+    }
+    return true;
+  default:
+    return false;
+  }
+}
 
+void
+ExprSMTLIBPrinter::setArrayValuesToGet(const std::vector<const Array *> &a) {
+  arraysToCallGetValueOn = &a;
+
+  // This option must be set in order to use the SMTLIBv2 command (get-value ()
+  // )
+  if (!a.empty())
+    setSMTLIBboolOption(PRODUCE_MODELS, OPTION_TRUE);
+
+  /* There is a risk that users will ask about array values that aren't
+   * even in the query. We should add them to the usedArrays list and hope
+   * that the solver knows what to do when we ask for the values of arrays
+   * that don't feature in our query!
+   */
+  for (vector<const Array *>::const_iterator i = a.begin(); i != a.end(); ++i) {
+    usedArrays.insert(*i);
+  }
+}
 
+const char *ExprSMTLIBPrinter::getSMTLIBOptionString(
+    ExprSMTLIBPrinter::SMTLIBboolOptions option) {
+  switch (option) {
+  case PRINT_SUCCESS:
+    return "print-success";
+  case PRODUCE_MODELS:
+    return "produce-models";
+  case INTERACTIVE_MODE:
+    return "interactive-mode";
+  default:
+    return "unknown-option";
+  }
+}
+}
diff --git a/test/Expr/print-smt.smt2.good b/test/Expr/print-smt.smt2.good
index cca282af..7b2002b9 100644
--- a/test/Expr/print-smt.smt2.good
+++ b/test/Expr/print-smt.smt2.good
@@ -859,9 +859,9 @@
 ;SMTLIBv2 Query 72
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun const_arr2 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (=  (select const_arr2 (_ bv0 32) ) (_ bv121 8) ) )
 (assert (=  (select const_arr2 (_ bv1 32) ) (_ bv101 8) ) )
 (assert (=  (select const_arr2 (_ bv2 32) ) (_ bv115 8) ) )
@@ -881,8 +881,8 @@
 ;SMTLIBv2 Query 73
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (let (  (?B0 ((_ extract 31  0)  (bvadd  (_ bv18446744073709533360 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) ) (?B1 (bvadd  (_ bv18446744073709533360 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (?B2 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (and (=  false (bvult  ?B2 (_ bv13 64) ) ) (and (=  false (bvult  (bvadd  (_ bv31312 64) ?B2 ) (_ bv1 64) ) ) (and (=  false (bvult  (bvadd  (_ bv31760 64) ?B2 ) (_ bv13 64) ) ) (and (=  false (bvult  (bvadd  (_ bv111120 64) ?B2 ) (_ bv1 64) ) ) (and (bvult  ?B1 (_ bv1 64) ) (=  false (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  unnamed (bvadd  (_ bv3 32) ?B0 ) ) (concat  (select  unnamed (bvadd  (_ bv2 32) ?B0 ) ) (concat  (select  unnamed (bvadd  (_ bv1 32) ?B0 ) ) (select  unnamed ?B0 ) ) ) ) ) ) ) ) ) ) ) )  )
 (check-sat)
 (get-value ( (select unnamed_1 (_ bv0 32) ) ) )
@@ -898,9 +898,9 @@
 ;SMTLIBv2 Query 74
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
-(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun const_arr5 () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (=  (select const_arr5 (_ bv0 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr5 (_ bv1 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr5 (_ bv2 32) ) (_ bv171 8) ) )
@@ -920,9 +920,9 @@
 ;SMTLIBv2 Query 75
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
-(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun const_arr1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (=  (select const_arr1 (_ bv0 32) ) (_ bv12 8) ) )
 (assert (=  (select const_arr1 (_ bv1 32) ) (_ bv0 8) ) )
 (assert (=  (select const_arr1 (_ bv2 32) ) (_ bv0 8) ) )
@@ -954,9 +954,9 @@
 ;SMTLIBv2 Query 76
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
-(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun const_arr4 () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (=  (select const_arr4 (_ bv0 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr4 (_ bv1 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr4 (_ bv2 32) ) (_ bv171 8) ) )
@@ -976,9 +976,9 @@
 ;SMTLIBv2 Query 77
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
-(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun const_arr3 () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (=  (select const_arr3 (_ bv0 32) ) (_ bv12 8) ) )
 (assert (=  (select const_arr3 (_ bv1 32) ) (_ bv0 8) ) )
 (assert (=  (select const_arr3 (_ bv2 32) ) (_ bv0 8) ) )
@@ -1010,8 +1010,8 @@
 ;SMTLIBv2 Query 78
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (let (  (?B0 ((_ extract 31  0)  (bvadd  (_ bv18446744073709532800 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) ) (?B1 (bvadd  (_ bv18446744073709532800 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (?B2 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (and (=  false (bvult  ?B2 (_ bv13 64) ) ) (and (=  false (bvult  (bvadd  (_ bv31312 64) ?B2 ) (_ bv1 64) ) ) (and (=  false (bvult  (bvadd  (_ bv31760 64) ?B2 ) (_ bv13 64) ) ) (and (=  false (bvult  (bvadd  (_ bv111120 64) ?B2 ) (_ bv1 64) ) ) (and (=  false (bvult  (bvadd  (_ bv18446744073709533360 64) ?B2 ) (_ bv1 64) ) ) (and (=  false (bvult  (bvadd  (_ bv18446744073709533328 64) ?B2 ) (_ bv1 64) ) ) (and (bvult  ?B1 (_ bv1 64) ) (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  unnamed_1 (bvadd  (_ bv3 32) ?B0 ) ) (concat  (select  unnamed_1 (bvadd  (_ bv2 32) ?B0 ) ) (concat  (select  unnamed_1 (bvadd  (_ bv1 32) ?B0 ) ) (select  unnamed_1 ?B0 ) ) ) ) ) ) ) ) ) ) ) ) )  )
 (check-sat)
 (get-value ( (select unnamed_1 (_ bv0 32) ) ) )