Nice patch by Dan Liew that adds support for printing queries in the

SMTLIB format (part of his MSc project work).


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166556 91177308-0d34-0410-b5e6-96231b3b80d8

4 files changed, 1524 insertions, 0 deletions

diff --git a/include/klee/util/ExprSMTLIBLetPrinter.h b/include/klee/util/ExprSMTLIBLetPrinter.h
new file mode 100644
index 00000000..56c8f008
--- /dev/null
+++ b/include/klee/util/ExprSMTLIBLetPrinter.h
@@ -0,0 +1,73 @@
+//===-- ExprSMTLIBLetPrinter.h ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "ExprSMTLIBPrinter.h"
+#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();
+
+		private:
+			///Let expression binding number map.
+			std::map<const ref<Expr>,unsigned int> bindings;
+
+			/* 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 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();
+}
+
+#endif /* EXPRSMTLETPRINTER_H_ */
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h
new file mode 100644
index 00000000..588d9d19
--- /dev/null
+++ b/include/klee/util/ExprSMTLIBPrinter.h
@@ -0,0 +1,296 @@
+//===-- ExprSMTLIBPrinter.h ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_EXPRSMTLIBPRINTER_H
+#define KLEE_EXPRSMTLIBPRINTER_H
+
+#include <ostream>
+#include <string>
+#include <set>
+#include <map>
+#include <klee/Constraints.h>
+#include <klee/Expr.h>
+#include <klee/util/PrintContext.h>
+#include <klee/Solver.h>
+
+namespace klee {
+
+	///Base Class for SMTLIBv2 printer for Expr trees. 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)
+	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 "mangled" query
+			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 mangleQuery()
+			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 mangleQuery();
+
+			//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
new file mode 100644
index 00000000..7225704e
--- /dev/null
+++ b/lib/Expr/ExprSMTLIBLetPrinter.cpp
@@ -0,0 +1,249 @@
+//===-- ExprSMTLIBLetPrinter.cpp ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include <iostream>
+#include "llvm/Support/CommandLine.h"
+#include "klee/util/ExprSMTLIBLetPrinter.h"
+
+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 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
new file mode 100644
index 00000000..aa75629a
--- /dev/null
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -0,0 +1,906 @@
+//===-- ExprSMTLIBPrinter.cpp ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+#include <iostream>
+
+#include "llvm/Support/Casting.h"
+#include "llvm/Support/CommandLine.h"
+#include "klee/util/ExprSMTLIBPrinter.h"
+
+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)
+
+
+	);
+
+	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();
+		mangleQuery();
+	}
+
+	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;
+	}
+
+
+	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::mangleQuery()
+	{
+		//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";
+	}
+}
+
+}
+
+
+