surprize surprize

14 files changed, 2202 insertions, 343 deletions

diff --git a/.cproject b/.cproject
index df8183d4e..ac930d8b9 100644
--- a/.cproject
+++ b/.cproject
@@ -2,319 +2,327 @@
 <?fileVersion 4.0.0?>
 
 <cproject storage_type_id="org.eclipse.cdt.core.XmlProjectDescriptionStorage">
-<storageModule moduleId="org.eclipse.cdt.core.settings">
-<cconfiguration id="cdt.managedbuild.toolchain.gnu.base.1461790692">
-<storageModule buildSystemId="org.eclipse.cdt.managedbuilder.core.configurationDataProvider" id="cdt.managedbuild.toolchain.gnu.base.1461790692" moduleId="org.eclipse.cdt.core.settings" name="Default">
-<externalSettings/>
-<extensions>
-<extension id="org.eclipse.cdt.core.ELF" point="org.eclipse.cdt.core.BinaryParser"/>
-<extension id="org.eclipse.cdt.core.MakeErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
-<extension id="org.eclipse.cdt.core.GCCErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
-<extension id="org.eclipse.cdt.core.GASErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
-<extension id="org.eclipse.cdt.core.GLDErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
-</extensions>
-</storageModule>
-<storageModule moduleId="cdtBuildSystem" version="4.0.0">
-<configuration artifactName="cvc4" buildProperties="" description="" id="cdt.managedbuild.toolchain.gnu.base.1461790692" name="Default" parent="org.eclipse.cdt.build.core.emptycfg">
-<folderInfo id="cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216" name="/" resourcePath="">
-<toolChain id="cdt.managedbuild.toolchain.gnu.base.1311293674" name="cdt.managedbuild.toolchain.gnu.base" superClass="cdt.managedbuild.toolchain.gnu.base">
-<targetPlatform archList="all" binaryParser="org.eclipse.cdt.core.ELF" id="cdt.managedbuild.target.gnu.platform.base.1799734525" name="Debug Platform" osList="linux,hpux,aix,qnx" superClass="cdt.managedbuild.target.gnu.platform.base"/>
-<builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="true" parallelizationNumber="2" superClass="cdt.managedbuild.target.gnu.builder.base">
-<outputEntries>
-<entry flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="outputPath" name=""/>
-</outputEntries>
-</builder>
-<tool id="cdt.managedbuild.tool.gnu.archiver.base.888684090" name="GCC Archiver" superClass="cdt.managedbuild.tool.gnu.archiver.base"/>
-<tool id="cdt.managedbuild.tool.gnu.cpp.compiler.base.1803857875" name="GCC C++ Compiler" superClass="cdt.managedbuild.tool.gnu.cpp.compiler.base">
-<inputType id="cdt.managedbuild.tool.gnu.cpp.compiler.input.1333398893" superClass="cdt.managedbuild.tool.gnu.cpp.compiler.input"/>
-</tool>
-<tool id="cdt.managedbuild.tool.gnu.c.compiler.base.1860041504" name="GCC C Compiler" superClass="cdt.managedbuild.tool.gnu.c.compiler.base">
-<inputType id="cdt.managedbuild.tool.gnu.c.compiler.input.814325769" superClass="cdt.managedbuild.tool.gnu.c.compiler.input"/>
-</tool>
-<tool id="cdt.managedbuild.tool.gnu.c.linker.base.1687463194" name="GCC C Linker" superClass="cdt.managedbuild.tool.gnu.c.linker.base"/>
-<tool id="cdt.managedbuild.tool.gnu.cpp.linker.base.709612973" name="GCC C++ Linker" superClass="cdt.managedbuild.tool.gnu.cpp.linker.base">
-<inputType id="cdt.managedbuild.tool.gnu.cpp.linker.input.399338768" superClass="cdt.managedbuild.tool.gnu.cpp.linker.input">
-<additionalInput kind="additionalinputdependency" paths="$(USER_OBJS)"/>
-<additionalInput kind="additionalinput" paths="$(LIBS)"/>
-</inputType>
-</tool>
-<tool id="cdt.managedbuild.tool.gnu.assembler.base.1211277012" name="GCC Assembler" superClass="cdt.managedbuild.tool.gnu.assembler.base">
-<inputType id="cdt.managedbuild.tool.gnu.assembler.input.330956883" superClass="cdt.managedbuild.tool.gnu.assembler.input"/>
-</tool>
-</toolChain>
-</folderInfo>
-<sourceEntries>
-<entry excluding="prop|parser|smt2" flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="sourcePath" name=""/>
-</sourceEntries>
-</configuration>
-</storageModule>
-<storageModule moduleId="org.eclipse.cdt.core.externalSettings"/>
-<storageModule moduleId="org.eclipse.cdt.internal.ui.text.commentOwnerProjectMappings"/>
-<storageModule moduleId="org.eclipse.cdt.core.language.mapping"/>
-<storageModule moduleId="org.eclipse.cdt.make.core.buildtargets">
-<buildTargets>
-<target name="check" path="" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
-<buildCommand>make</buildCommand>
-<buildArguments/>
-<buildTarget>check</buildTarget>
-<stopOnError>true</stopOnError>
-<useDefaultCommand>true</useDefaultCommand>
-<runAllBuilders>true</runAllBuilders>
-</target>
-</buildTargets>
-</storageModule>
-<storageModule moduleId="scannerConfiguration">
-<autodiscovery enabled="true" problemReportingEnabled="true" selectedProfileId=""/>
-<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerFileProfile">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="makefileGenerator">
-<runAction arguments="-f ${project_name}_scd.mk" command="make" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfile">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.cpp" command="g++" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.c" command="gcc" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfile">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-c 'gcc -E -P -v -dD &quot;${plugin_state_location}/${specs_file}&quot;'" command="sh" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileCPP">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-c 'g++ -E -P -v -dD &quot;${plugin_state_location}/specs.cpp&quot;'" command="sh" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileC">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-c 'gcc -E -P -v -dD &quot;${plugin_state_location}/specs.c&quot;'" command="sh" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<scannerConfigBuildInfo instanceId="cdt.managedbuild.toolchain.gnu.base.1461790692;cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216;cdt.managedbuild.tool.gnu.cpp.compiler.base.1803857875;cdt.managedbuild.tool.gnu.cpp.compiler.input.1333398893">
-<autodiscovery enabled="true" problemReportingEnabled="false" selectedProfileId="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP"/>
-<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerFileProfile">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="makefileGenerator">
-<runAction arguments="-f ${project_name}_scd.mk" command="make" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfile">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.cpp" command="g++" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.c" command="gcc" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfile">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-c 'gcc -E -P -v -dD &quot;${plugin_state_location}/${specs_file}&quot;'" command="sh" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileCPP">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-c 'g++ -E -P -v -dD &quot;${plugin_state_location}/specs.cpp&quot;'" command="sh" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileC">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-c 'gcc -E -P -v -dD &quot;${plugin_state_location}/specs.c&quot;'" command="sh" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-</scannerConfigBuildInfo>
-<scannerConfigBuildInfo instanceId="cdt.managedbuild.toolchain.gnu.base.1461790692;cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216;cdt.managedbuild.tool.gnu.c.compiler.base.1860041504;cdt.managedbuild.tool.gnu.c.compiler.input.814325769">
-<autodiscovery enabled="true" problemReportingEnabled="false" selectedProfileId="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC"/>
-<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerFileProfile">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="makefileGenerator">
-<runAction arguments="-f ${project_name}_scd.mk" command="make" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfile">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.cpp" command="g++" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.c" command="gcc" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfile">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-c 'gcc -E -P -v -dD &quot;${plugin_state_location}/${specs_file}&quot;'" command="sh" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileCPP">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-c 'g++ -E -P -v -dD &quot;${plugin_state_location}/specs.cpp&quot;'" command="sh" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileC">
-<buildOutputProvider>
-<openAction enabled="true" filePath=""/>
-<parser enabled="true"/>
-</buildOutputProvider>
-<scannerInfoProvider id="specsFile">
-<runAction arguments="-c 'gcc -E -P -v -dD &quot;${plugin_state_location}/specs.c&quot;'" command="sh" useDefault="true"/>
-<parser enabled="true"/>
-</scannerInfoProvider>
-</profile>
-</scannerConfigBuildInfo>
-</storageModule>
-</cconfiguration>
-</storageModule>
-<storageModule moduleId="cdtBuildSystem" version="4.0.0">
-<project id="cvc4.null.1129006228" name="cvc4"/>
-</storageModule>
+	<storageModule moduleId="org.eclipse.cdt.core.settings">
+		<cconfiguration id="cdt.managedbuild.toolchain.gnu.base.1461790692">
+			<storageModule buildSystemId="org.eclipse.cdt.managedbuilder.core.configurationDataProvider" id="cdt.managedbuild.toolchain.gnu.base.1461790692" moduleId="org.eclipse.cdt.core.settings" name="Default">
+				<externalSettings/>
+				<extensions>
+					<extension id="org.eclipse.cdt.core.ELF" point="org.eclipse.cdt.core.BinaryParser"/>
+					<extension id="org.eclipse.cdt.core.GCCErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
+					<extension id="org.eclipse.cdt.core.GASErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
+					<extension id="org.eclipse.cdt.core.GLDErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
+					<extension id="org.eclipse.cdt.core.GmakeErrorParser" point="org.eclipse.cdt.core.ErrorParser"/>
+					<extension id="org.eclipse.cdt.core.CWDLocator" point="org.eclipse.cdt.core.ErrorParser"/>
+				</extensions>
+			</storageModule>
+			<storageModule moduleId="cdtBuildSystem" version="4.0.0">
+				<configuration artifactName="cvc4" buildProperties="" description="" id="cdt.managedbuild.toolchain.gnu.base.1461790692" name="Default" parent="org.eclipse.cdt.build.core.emptycfg">
+					<folderInfo id="cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216" name="/" resourcePath="">
+						<toolChain id="cdt.managedbuild.toolchain.gnu.base.1311293674" name="cdt.managedbuild.toolchain.gnu.base" superClass="cdt.managedbuild.toolchain.gnu.base">
+							<targetPlatform archList="all" binaryParser="org.eclipse.cdt.core.ELF" id="cdt.managedbuild.target.gnu.platform.base.1799734525" name="Debug Platform" osList="linux,hpux,aix,qnx" superClass="cdt.managedbuild.target.gnu.platform.base"/>
+							<builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="true" parallelizationNumber="2" superClass="cdt.managedbuild.target.gnu.builder.base">
+								<outputEntries>
+									<entry flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="outputPath" name=""/>
+								</outputEntries>
+							</builder>
+							<tool id="cdt.managedbuild.tool.gnu.archiver.base.888684090" name="GCC Archiver" superClass="cdt.managedbuild.tool.gnu.archiver.base"/>
+							<tool id="cdt.managedbuild.tool.gnu.cpp.compiler.base.1803857875" name="GCC C++ Compiler" superClass="cdt.managedbuild.tool.gnu.cpp.compiler.base">
+								<inputType id="cdt.managedbuild.tool.gnu.cpp.compiler.input.1333398893" superClass="cdt.managedbuild.tool.gnu.cpp.compiler.input"/>
+							</tool>
+							<tool id="cdt.managedbuild.tool.gnu.c.compiler.base.1860041504" name="GCC C Compiler" superClass="cdt.managedbuild.tool.gnu.c.compiler.base">
+								<inputType id="cdt.managedbuild.tool.gnu.c.compiler.input.814325769" superClass="cdt.managedbuild.tool.gnu.c.compiler.input"/>
+							</tool>
+							<tool id="cdt.managedbuild.tool.gnu.c.linker.base.1687463194" name="GCC C Linker" superClass="cdt.managedbuild.tool.gnu.c.linker.base"/>
+							<tool id="cdt.managedbuild.tool.gnu.cpp.linker.base.709612973" name="GCC C++ Linker" superClass="cdt.managedbuild.tool.gnu.cpp.linker.base">
+								<inputType id="cdt.managedbuild.tool.gnu.cpp.linker.input.399338768" superClass="cdt.managedbuild.tool.gnu.cpp.linker.input">
+									<additionalInput kind="additionalinputdependency" paths="$(USER_OBJS)"/>
+									<additionalInput kind="additionalinput" paths="$(LIBS)"/>
+								</inputType>
+							</tool>
+							<tool id="cdt.managedbuild.tool.gnu.assembler.base.1211277012" name="GCC Assembler" superClass="cdt.managedbuild.tool.gnu.assembler.base">
+								<inputType id="cdt.managedbuild.tool.gnu.assembler.input.330956883" superClass="cdt.managedbuild.tool.gnu.assembler.input"/>
+							</tool>
+						</toolChain>
+					</folderInfo>
+					<sourceEntries>
+						<entry excluding="prop|parser|smt2" flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="sourcePath" name=""/>
+					</sourceEntries>
+				</configuration>
+			</storageModule>
+			<storageModule moduleId="org.eclipse.cdt.core.externalSettings"/>
+			<storageModule moduleId="org.eclipse.cdt.internal.ui.text.commentOwnerProjectMappings"/>
+			<storageModule moduleId="org.eclipse.cdt.core.language.mapping"/>
+			<storageModule moduleId="scannerConfiguration">
+				<autodiscovery enabled="true" problemReportingEnabled="true" selectedProfileId=""/>
+				<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile">
+					<buildOutputProvider>
+						<openAction enabled="true" filePath=""/>
+						<parser enabled="true"/>
+					</buildOutputProvider>
+					<scannerInfoProvider id="specsFile">
+						<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/>
+						<parser enabled="true"/>
+					</scannerInfoProvider>
+				</profile>
+				<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerFileProfile">
+					<buildOutputProvider>
+						<openAction enabled="true" filePath=""/>
+						<parser enabled="true"/>
+					</buildOutputProvider>
+					<scannerInfoProvider id="makefileGenerator">
+						<runAction arguments="-f ${project_name}_scd.mk" command="make" useDefault="true"/>
+						<parser enabled="true"/>
+					</scannerInfoProvider>
+				</profile>
+				<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfile">
+					<buildOutputProvider>
+						<openAction enabled="true" filePath=""/>
+						<parser enabled="true"/>
+					</buildOutputProvider>
+					<scannerInfoProvider id="specsFile">
+						<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/>
+						<parser enabled="true"/>
+					</scannerInfoProvider>
+				</profile>
+				<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP">
+					<buildOutputProvider>
+						<openAction enabled="true" filePath=""/>
+						<parser enabled="true"/>
+					</buildOutputProvider>
+					<scannerInfoProvider id="specsFile">
+						<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.cpp" command="g++" useDefault="true"/>
+						<parser enabled="true"/>
+					</scannerInfoProvider>
+				</profile>
+				<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC">
+					<buildOutputProvider>
+						<openAction enabled="true" filePath=""/>
+						<parser enabled="true"/>
+					</buildOutputProvider>
+					<scannerInfoProvider id="specsFile">
+						<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.c" command="gcc" useDefault="true"/>
+						<parser enabled="true"/>
+					</scannerInfoProvider>
+				</profile>
+				<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfile">
+					<buildOutputProvider>
+						<openAction enabled="true" filePath=""/>
+						<parser enabled="true"/>
+					</buildOutputProvider>
+					<scannerInfoProvider id="specsFile">
+						<runAction arguments="-c 'gcc -E -P -v -dD &quot;${plugin_state_location}/${specs_file}&quot;'" command="sh" useDefault="true"/>
+						<parser enabled="true"/>
+					</scannerInfoProvider>
+				</profile>
+				<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileCPP">
+					<buildOutputProvider>
+						<openAction enabled="true" filePath=""/>
+						<parser enabled="true"/>
+					</buildOutputProvider>
+					<scannerInfoProvider id="specsFile">
+						<runAction arguments="-c 'g++ -E -P -v -dD &quot;${plugin_state_location}/specs.cpp&quot;'" command="sh" useDefault="true"/>
+						<parser enabled="true"/>
+					</scannerInfoProvider>
+				</profile>
+				<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileC">
+					<buildOutputProvider>
+						<openAction enabled="true" filePath=""/>
+						<parser enabled="true"/>
+					</buildOutputProvider>
+					<scannerInfoProvider id="specsFile">
+						<runAction arguments="-c 'gcc -E -P -v -dD &quot;${plugin_state_location}/specs.c&quot;'" command="sh" useDefault="true"/>
+						<parser enabled="true"/>
+					</scannerInfoProvider>
+				</profile>
+				<scannerConfigBuildInfo instanceId="cdt.managedbuild.toolchain.gnu.base.1461790692;cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216;cdt.managedbuild.tool.gnu.cpp.compiler.base.1803857875;cdt.managedbuild.tool.gnu.cpp.compiler.input.1333398893">
+					<autodiscovery enabled="true" problemReportingEnabled="false" selectedProfileId="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP"/>
+					<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="specsFile">
+							<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+					<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerFileProfile">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="makefileGenerator">
+							<runAction arguments="-f ${project_name}_scd.mk" command="make" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+					<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfile">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="specsFile">
+							<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+					<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="specsFile">
+							<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.cpp" command="g++" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+					<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="specsFile">
+							<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.c" command="gcc" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+					<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfile">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="specsFile">
+							<runAction arguments="-c 'gcc -E -P -v -dD &quot;${plugin_state_location}/${specs_file}&quot;'" command="sh" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+					<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileCPP">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="specsFile">
+							<runAction arguments="-c 'g++ -E -P -v -dD &quot;${plugin_state_location}/specs.cpp&quot;'" command="sh" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+					<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileC">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="specsFile">
+							<runAction arguments="-c 'gcc -E -P -v -dD &quot;${plugin_state_location}/specs.c&quot;'" command="sh" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+				</scannerConfigBuildInfo>
+				<scannerConfigBuildInfo instanceId="cdt.managedbuild.toolchain.gnu.base.1461790692;cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216;cdt.managedbuild.tool.gnu.c.compiler.base.1860041504;cdt.managedbuild.tool.gnu.c.compiler.input.814325769">
+					<autodiscovery enabled="true" problemReportingEnabled="false" selectedProfileId="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC"/>
+					<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerProjectProfile">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="specsFile">
+							<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+					<profile id="org.eclipse.cdt.make.core.GCCStandardMakePerFileProfile">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="makefileGenerator">
+							<runAction arguments="-f ${project_name}_scd.mk" command="make" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+					<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfile">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="specsFile">
+							<runAction arguments="-E -P -v -dD ${plugin_state_location}/${specs_file}" command="gcc" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+					<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileCPP">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="specsFile">
+							<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.cpp" command="g++" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+					<profile id="org.eclipse.cdt.managedbuilder.core.GCCManagedMakePerProjectProfileC">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="specsFile">
+							<runAction arguments="-E -P -v -dD ${plugin_state_location}/specs.c" command="gcc" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+					<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfile">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="specsFile">
+							<runAction arguments="-c 'gcc -E -P -v -dD &quot;${plugin_state_location}/${specs_file}&quot;'" command="sh" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+					<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileCPP">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="specsFile">
+							<runAction arguments="-c 'g++ -E -P -v -dD &quot;${plugin_state_location}/specs.cpp&quot;'" command="sh" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+					<profile id="org.eclipse.cdt.managedbuilder.core.GCCWinManagedMakePerProjectProfileC">
+						<buildOutputProvider>
+							<openAction enabled="true" filePath=""/>
+							<parser enabled="true"/>
+						</buildOutputProvider>
+						<scannerInfoProvider id="specsFile">
+							<runAction arguments="-c 'gcc -E -P -v -dD &quot;${plugin_state_location}/specs.c&quot;'" command="sh" useDefault="true"/>
+							<parser enabled="true"/>
+						</scannerInfoProvider>
+					</profile>
+				</scannerConfigBuildInfo>
+			</storageModule>
+			<storageModule moduleId="org.eclipse.cdt.make.core.buildtargets">
+				<buildTargets>
+					<target name="check" path="" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
+						<buildCommand>make</buildCommand>
+						<buildTarget>check</buildTarget>
+						<stopOnError>true</stopOnError>
+						<useDefaultCommand>true</useDefaultCommand>
+						<runAllBuilders>true</runAllBuilders>
+					</target>
+					<target name="uf" path="src/theory/uf" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
+						<buildCommand>make</buildCommand>
+						<buildArguments>-j2</buildArguments>
+						<buildTarget/>
+						<stopOnError>true</stopOnError>
+						<useDefaultCommand>true</useDefaultCommand>
+						<runAllBuilders>true</runAllBuilders>
+					</target>
+				</buildTargets>
+			</storageModule>
+		</cconfiguration>
+	</storageModule>
+	<storageModule moduleId="cdtBuildSystem" version="4.0.0">
+		<project id="cvc4.null.1129006228" name="cvc4"/>
+	</storageModule>
 </cproject>
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 4ed5a3ac7..ced34b8be 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -11,7 +11,7 @@ libexpr_la_SOURCES = \
 	type_node.h \
 	type_node.cpp \
 	node_builder.h \
-	convenience_node_builders.h \
+	convenience_node_builders.h \	
 	type.h \
 	type.cpp \
 	node_value.h \
@@ -27,7 +27,9 @@ libexpr_la_SOURCES = \
 	declaration_scope.cpp \
 	expr_manager_scope.h \
 	node_self_iterator.h \
-	expr_stream.h
+	expr_stream.h \
+	kind_map.h
+	
 nodist_libexpr_la_SOURCES = \
 	kind.h \
 	metakind.h \
diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h
new file mode 100644
index 000000000..a02339e5e
--- /dev/null
+++ b/src/expr/kind_map.h
@@ -0,0 +1,275 @@
+/*********************                                                        */
+/*! \file kind_map.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A bitmap of Kinds
+ **
+ ** This is a class representation for a bitmap of Kinds that is
+ ** iterable, manipulable, and packed.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__KIND_MAP_H
+#define __CVC4__KIND_MAP_H
+
+#include <stdint.h>
+#include <iterator>
+
+#include "expr/kind.h"
+
+namespace CVC4 {
+
+/** A bitmap of Kinds. */
+class KindMap {
+  static const size_t SIZE = (kind::LAST_KIND + 63) / 64;
+
+  uint64_t d_bitmap[SIZE];
+
+  /**
+   * Accessor proxy class used so that things like "map[k] = true"
+   * will work as expected (we have to return a proxy from
+   * KindMap::operator[]() in that case, since we can't construct an
+   * address to the individual *bit* in the packed representation).
+   */
+  class Accessor {
+    KindMap& d_map;
+    Kind d_kind;
+
+    Accessor(KindMap& m, Kind k) :
+      d_map(m),
+      d_kind(k) {
+      AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind");
+    }
+
+    friend class KindMap;
+
+  public:
+
+    operator bool() const {
+      return d_map.tst(d_kind);
+    }
+
+    Accessor operator=(bool b) const {
+      if(b) {
+        d_map.set(d_kind);
+      } else {
+        d_map.clr(d_kind);
+      }
+      return *this;
+    }
+
+  };/* class KindMap::Accessor */
+
+public:
+
+  /** An iterator over a KindMap. */
+  class iterator {
+    const KindMap* d_map;
+    Kind d_kind;
+
+  public:
+    typedef std::input_iterator_tag iterator_category;
+    typedef Kind value_type;
+
+    iterator() :
+      d_map(NULL),
+      d_kind(Kind(0)) {
+    }
+    iterator(const KindMap& m, Kind k) :
+      d_map(&m),
+      d_kind(k) {
+      AssertArgument(k >= Kind(0) && k <= kind::LAST_KIND, k, "invalid kind");
+      while(d_kind < kind::LAST_KIND &&
+            ! d_map->tst(d_kind)) {
+        d_kind = Kind(uint64_t(d_kind) + 1);
+      }
+    }
+    iterator& operator++() {
+      if(d_kind < kind::LAST_KIND) {
+        d_kind = Kind(uint64_t(d_kind) + 1);
+        while(d_kind < kind::LAST_KIND &&
+              ! d_map->tst(d_kind)) {
+          d_kind = Kind(uint64_t(d_kind) + 1);
+        }
+      }
+      return *this;
+    }
+    iterator operator++(int) const {
+      const_iterator i = *this;
+      ++i;
+      return i;
+    }
+    Kind operator*() const {
+      return d_kind;
+    }
+    bool operator==(iterator i) const {
+      return d_map == i.d_map && d_kind == i.d_kind;
+    }
+    bool operator!=(iterator i) const {
+      return !(*this == i);
+    }
+  };/* class KindMap::iterator */
+  typedef iterator const_iterator;
+
+  KindMap() {
+    clear();
+  }
+  KindMap(const KindMap& m) {
+    for(unsigned i = 0; i < SIZE; ++i) {
+      d_bitmap[i] = m.d_bitmap[i];
+    }
+  }
+  KindMap(Kind k) {
+    clear();
+    set(k);
+  }
+
+  /** Empty the map. */
+  void clear() {
+    for(unsigned i = 0; i < SIZE; ++i) {
+      d_bitmap[i] = uint64_t(0);
+    }
+  }
+  /** Tests whether the map is empty. */
+  bool isEmpty() const {
+    for(unsigned i = 0; i < SIZE; ++i) {
+      if(d_bitmap[i] != uint64_t(0)) {
+        return false;
+      }
+    }
+    return true;
+  }
+  /** Test whether k is in the map. */
+  bool tst(Kind k) const {
+    AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind");
+    return (d_bitmap[k / 64] >> (k % 64)) & uint64_t(1);
+  }
+  /** Set k in the map. */
+  void set(Kind k) {
+    AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind");
+    d_bitmap[k / 64] |= (uint64_t(1) << (k % 64));
+  }
+  /** Clear k from the map. */
+  void clr(Kind k) {
+    AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind");
+    d_bitmap[k / 64] &= ~(uint64_t(1) << (k % 64));
+  }
+
+  /** Iterate over the map. */
+  const_iterator begin() const {
+    return const_iterator(*this, Kind(0));
+  }
+  const_iterator end() const {
+    return const_iterator(*this, kind::LAST_KIND);
+  }
+
+  /** Invert the map. */
+  KindMap operator~() const {
+    KindMap r;
+    for(unsigned i = 0; i < SIZE; ++i) {
+      r.d_bitmap[i] = ~d_bitmap[i];
+    }
+    return r;
+  }
+  /** Bitwise-AND the map (with assignment). */
+  KindMap& operator&=(const KindMap& m) {
+    for(unsigned i = 0; i < SIZE; ++i) {
+      d_bitmap[i] &= m.d_bitmap[i];
+    }
+    return *this;
+  }
+  /** Bitwise-AND the map. */
+  KindMap operator&(const KindMap& m) const {
+    KindMap r(*this);
+    r &= m;
+    return r;
+  }
+  /** Bitwise-OR the map (with assignment). */
+  KindMap& operator|=(const KindMap& m) {
+    for(unsigned i = 0; i < SIZE; ++i) {
+      d_bitmap[i] |= m.d_bitmap[i];
+    }
+    return *this;
+  }
+  /** Bitwise-OR the map. */
+  KindMap operator|(const KindMap& m) const {
+    KindMap r(*this);
+    r |= m;
+    return r;
+  }
+  /** Bitwise-XOR the map (with assignment). */
+  KindMap& operator^=(const KindMap& m) {
+    for(unsigned i = 0; i < SIZE; ++i) {
+      d_bitmap[i] ^= m.d_bitmap[i];
+    }
+    return *this;
+  }
+  /** Bitwise-XOR the map. */
+  KindMap operator^(const KindMap& m) const {
+    KindMap r(*this);
+    r ^= m;
+    return r;
+  }
+
+  /** Test whether k is in the map. */
+  bool operator[](Kind k) const {
+    return tst(k);
+  }
+  /** Test whether k is in the map (allowing assignment). */
+  Accessor operator[](Kind k) {
+    return Accessor(*this, k);
+  }
+
+  /** Test equality between two maps. */
+  bool operator==(KindMap m) {
+    for(unsigned i = 0; i < SIZE; ++i) {
+      if(d_bitmap[i] != m.d_bitmap[i]) {
+        return false;
+      }
+    }
+    return true;
+  }
+  bool operator!=(KindMap m) {
+    return !(*this == m);
+  }
+};/* class KindMap */
+
+inline KindMap operator~(Kind k) {
+  KindMap m(k);
+  return ~m;
+}
+inline KindMap operator&(Kind k1, Kind k2) {
+  KindMap m(k1);
+  return m &= k2;
+}
+inline KindMap operator&(Kind k1, KindMap m2) {
+  return m2 & k1;
+}
+inline KindMap operator|(Kind k1, Kind k2) {
+  KindMap m(k1);
+  return m |= k2;
+}
+inline KindMap operator|(Kind k1, KindMap m2) {
+  return m2 | k1;
+}
+inline KindMap operator^(Kind k1, Kind k2) {
+  KindMap m(k1);
+  return m ^= k2;
+}
+inline KindMap operator^(Kind k1, KindMap m2) {
+  return m2 ^ k1;
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__KIND_MAP_H */
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 7e335a21b..cbec9faea 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -154,6 +154,24 @@ Node PropEngine::getValue(TNode node) {
   }
 }
 
+bool PropEngine::hasValue(TNode node, bool& value) {
+  Assert(node.getType().isBoolean());
+  SatLiteral lit = d_cnfStream->getLiteral(node);
+
+  SatLiteralValue v = d_satSolver->value(lit);
+  if(v == l_True) {
+    value = true;
+    return true;
+  } else if(v == l_False) {
+    value = false;
+    return true;
+  } else {
+    Assert(v == l_Undef);
+    return false;
+  }
+}
+
+
 void PropEngine::push() {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
   d_satSolver->push();
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index e1a1c08d7..f44ad16f7 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -115,6 +115,11 @@ public:
   Node getValue(TNode node);
 
   /**
+   * Check if the node has a value and return it if yes.
+   */
+  bool hasValue(TNode node, bool& value);
+
+  /**
    * Push the context level.
    */
   void push();
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4185765a8..d85f28b23 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -45,8 +45,6 @@
 #include "theory/booleans/theory_bool.h"
 #include "theory/booleans/circuit_propagator.h"
 #include "theory/uf/theory_uf.h"
-#include "theory/uf/morgan/theory_uf_morgan.h"
-#include "theory/uf/tim/theory_uf_tim.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/arrays/theory_arrays.h"
 #include "theory/bv/theory_bv.h"
@@ -199,16 +197,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_theoryEngine->addTheory<theory::arrays::TheoryArrays>();
   d_theoryEngine->addTheory<theory::bv::TheoryBV>();
   d_theoryEngine->addTheory<theory::datatypes::TheoryDatatypes>();
-  switch(Options::current()->uf_implementation) {
-  case Options::TIM:
-    d_theoryEngine->addTheory<theory::uf::tim::TheoryUFTim>();
-    break;
-  case Options::MORGAN:
-    d_theoryEngine->addTheory<theory::uf::morgan::TheoryUFMorgan>();
-    break;
-  default:
-    Unhandled(Options::current()->uf_implementation);
-  }
+  d_theoryEngine->addTheory<theory::uf::TheoryUF>();
 
   d_propEngine = new PropEngine(d_theoryEngine, d_context);
   d_theoryEngine->setPropEngine(d_propEngine);
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index e4647b442..3cf53960a 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -11,6 +11,7 @@ nodist_EXTRA_libuf_la_SOURCES = \
 
 libuf_la_SOURCES = \
 	theory_uf.h \
+	theory_uf.cpp \
 	theory_uf_type_rules.h \
 	theory_uf_rewriter.h
 
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
new file mode 100644
index 000000000..ac02fe4db
--- /dev/null
+++ b/src/theory/uf/equality_engine.h
@@ -0,0 +1,555 @@
+/*********************                                                        */
+/*! \file equality_engine.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <queue>
+#include <vector>
+#include <ext/hash_map>
+#include <sstream>
+
+#include "expr/node.h"
+#include "expr/kind_map.h"
+#include "context/cdo.h"
+#include "util/output.h"
+#include "util/stats.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+/** Id of the node */
+typedef size_t EqualityNodeId;
+
+/** Id of the use list */
+typedef size_t UseListNodeId;
+
+/** The trigger ids */
+typedef size_t TriggerId;
+
+/** The equality edge ids */
+typedef size_t EqualityEdgeId;
+
+/** The null node */
+static const EqualityNodeId null_id = (size_t)(-1);
+
+/** The null use list node */
+static const EqualityNodeId null_uselist_id = (size_t)(-1);
+
+/** The null trigger */
+static const TriggerId null_trigger = (size_t)(-1);
+
+/** The null edge id */
+static const EqualityEdgeId null_edge = (size_t)(-1);
+
+/**
+ * A reason for a merge. Either an equality x = y, or a merge of two
+ * function applications f(x1, x2), f(y1, y2)
+ */
+enum MergeReasonType {
+  MERGED_THROUGH_CONGRUENCE,
+  MERGED_THROUGH_EQUALITY
+};
+
+inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
+  switch (reason) {
+  case MERGED_THROUGH_CONGRUENCE:
+    out << "c";
+    break;
+  case MERGED_THROUGH_EQUALITY:
+    out << "e";
+    break;
+  default:
+    Unreachable();
+  }
+  return out;
+}
+
+/** A node in the uselist */
+class UseListNode {
+
+private:
+
+  /** The id of the application node where this representative is at */
+  EqualityNodeId d_applicationId;
+
+  /** The next one in the class */
+  UseListNodeId d_nextUseListNodeId;
+
+public:
+
+  /**
+   * Creates a new node, which is in a list of it's own.
+   */
+  UseListNode(EqualityNodeId nodeId, UseListNodeId nextId)
+  : d_applicationId(nodeId), d_nextUseListNodeId(nextId) {}
+
+  /**
+   * Returns the next node in the circular list.
+   */
+  UseListNodeId getNext() const {
+    return d_nextUseListNodeId;
+  }
+
+  /**
+   * Returns the id of the function application.
+   */
+  EqualityNodeId getApplicationId() const {
+    return d_applicationId;
+  }
+};
+
+
+class EqualityNode {
+
+private:
+
+  /** The size of this equivalence class (if it's a representative) */
+  size_t d_size;
+
+  /** The id (in the eq-manager) of the representative equality node */
+  EqualityNodeId d_findId;
+
+  /** The next equality node in this class */
+  EqualityNodeId d_nextId;
+
+  /** The use list of this node */
+  UseListNodeId d_useList;
+
+public:
+
+  /**
+   * Creates a new node, which is in a list of it's own.
+   */
+  EqualityNode(EqualityNodeId nodeId = null_id)
+  : d_size(1), d_findId(nodeId), d_nextId(nodeId), d_useList(null_uselist_id) {}
+
+  /**
+   * Retuerns the uselist.
+   */
+  UseListNodeId getUseList() const {
+    return d_useList;
+  }
+
+  /**
+   * Returns the next node in the class circular list.
+   */
+  EqualityNodeId getNext() const {
+    return d_nextId;
+  }
+
+  /**
+   * Returns the size of this equivalence class (only valid if this is the representative).
+   */
+  size_t getSize() const {
+    return d_size;
+  }
+
+  /**
+   * Merges the two lists. If add size is true the size of this node is increased by the size of
+   * the other node, otherwise the size is decreased by the size of the other node.
+   */
+  template<bool addSize>
+  void merge(EqualityNode& other) {
+    EqualityNodeId tmp = d_nextId; d_nextId = other.d_nextId; other.d_nextId = tmp;
+    if (addSize) {
+      d_size += other.d_size;
+    } else {
+      d_size -= other.d_size;
+    }
+  }
+
+  /**
+   * Returns the class representative.
+   */
+  EqualityNodeId getFind() const { return d_findId; }
+
+  /**
+   * Set the class representative.
+   */
+  void setFind(EqualityNodeId findId) { d_findId = findId; }
+
+  /**
+   * Note that this node is used in a function a application funId.
+   */
+  template<typename memory_class>
+  void usedIn(EqualityNodeId funId, memory_class& memory) {
+    UseListNodeId newUseId = memory.size();
+    memory.push_back(UseListNode(funId, d_useList));
+    d_useList = newUseId;
+  }
+
+};
+
+template <typename NotifyClass>
+class EqualityEngine {
+
+public:
+
+  /** Statistics about the equality engine instance */
+  struct Statistics {
+    /** Total number of merges */
+    IntStat mergesCount;
+    /** Number of terms managed by the system */
+    IntStat termsCount;
+    /** Number of function terms managed by the system */
+    IntStat functionTermsCount;
+    /** Number of times we performed a backtrack */
+    IntStat backtracksCount;
+
+    Statistics(std::string name)
+    : mergesCount(name + "::mergesCount", 0),
+      termsCount(name + "::termsCount", 0),
+      functionTermsCount(name + "::functionTermsCount", 0),
+      backtracksCount(name + "::backtracksCount", 0)
+    {
+      StatisticsRegistry::registerStat(&mergesCount);
+      StatisticsRegistry::registerStat(&termsCount);
+      StatisticsRegistry::registerStat(&functionTermsCount);
+      StatisticsRegistry::registerStat(&backtracksCount);
+    }
+
+    ~Statistics() {
+      StatisticsRegistry::unregisterStat(&mergesCount);
+      StatisticsRegistry::unregisterStat(&termsCount);
+      StatisticsRegistry::unregisterStat(&functionTermsCount);
+      StatisticsRegistry::unregisterStat(&backtracksCount);
+    }
+  };
+
+  /**
+   * f(a,b)
+   */
+  struct FunctionApplication {
+    EqualityNodeId a, b;
+    FunctionApplication(EqualityNodeId a = null_id, EqualityNodeId b = null_id):
+      a(a), b(b) {}
+    bool operator == (const FunctionApplication& other) const {
+      return a == other.a && b == other.b;
+    }
+    bool isApplication() {
+      return a != null_id && b != null_id;
+    }
+  };
+
+  struct FunctionApplicationHashFunction {
+    size_t operator () (const FunctionApplication& app) const {
+      size_t hash = 0;
+      hash = 0x9e3779b9 + app.a;
+      hash ^= 0x9e3779b9 + app.b + (hash << 6) + (hash >> 2);
+      return hash;
+    }
+  };
+
+private:
+
+  /** The class to notify when a representative changes for a term */
+  NotifyClass d_notify;
+
+  /** The map of kinds to be treated as function applications */
+  KindMap d_congruenceKinds;
+
+  /** Map from nodes to their ids */
+  __gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
+
+  /** Map from function applications to their ids */
+  typedef __gnu_cxx::hash_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> ApplicationIdsMap;
+
+  /**
+   * A map from a pair (a', b') to a function application f(a, b), where a' and b' are the current representatives
+   * of a and b.
+   */
+  ApplicationIdsMap d_applicationLookup;
+
+  /** Map from ids to the nodes */
+  std::vector<TNode> d_nodes;
+
+  /** Map from ids to the nodes */
+  std::vector<FunctionApplication> d_applications;
+
+  /** Map from ids to the equality nodes */
+  std::vector<EqualityNode> d_equalityNodes;
+
+  /** Memory for the use-list nodes */
+  std::vector<UseListNode> d_useListNodes;
+
+  /** Number of asserted equalities we have so far */
+  context::CDO<size_t> d_assertedEqualitiesCount;
+
+  /**
+   * We keep a list of asserted equalities. Not among original terms, but
+   * among the class representatives.
+   */
+  struct Equality {
+    /** Left hand side of the equality */
+    EqualityNodeId lhs;
+    /** Right hand side of the equality */
+    EqualityNodeId rhs;
+    /** Equality constructor */
+    Equality(EqualityNodeId lhs = null_id, EqualityNodeId rhs = null_id)
+    : lhs(lhs), rhs(rhs) {}
+  };
+
+  /** The ids of the classes we have merged */
+  std::vector<Equality> d_assertedEqualities;
+
+  /** The reasons for the equalities */
+
+  /**
+   * An edge in the equality graph. This graph is an undirected graph (both edges added)
+   * containing the actual asserted equalities.
+   */
+  class EqualityEdge {
+
+    // The id of the RHS of this equality
+    EqualityNodeId d_nodeId;
+    // The next edge
+    EqualityEdgeId d_nextId;
+    // Type of reason for this equality
+    MergeReasonType d_mergeType;
+    // Reason of this equality
+    TNode d_reason;
+
+  public:
+
+    EqualityEdge():
+      d_nodeId(null_edge), d_nextId(null_edge), d_mergeType(MERGED_THROUGH_CONGRUENCE) {}
+
+    EqualityEdge(EqualityNodeId nodeId, EqualityNodeId nextId, MergeReasonType type, TNode reason):
+      d_nodeId(nodeId), d_nextId(nextId), d_mergeType(type), d_reason(reason) {}
+
+    /** Returns the id of the next edge */
+    EqualityEdgeId getNext() const { return d_nextId; }
+
+    /** Returns the id of the target edge node */
+    EqualityNodeId getNodeId() const { return d_nodeId; }
+
+    /** The reason of this edge */
+    MergeReasonType getReasonType() const { return d_mergeType; }
+
+    /** The reason of this edge */
+    TNode getReason() const { return d_reason; }
+};
+
+  /**
+   * All the equality edges (twice as many as the number of asserted equalities. If an equality
+   * t1 = t2 is asserted, the edges added are -> t2, -> t1 (in this order). Hance, having the index
+   * of one of the edges you can reconstruct the original equality.
+   */
+  std::vector<EqualityEdge> d_equalityEdges;
+
+  /**
+   * Returns the string representation of the edges.
+   */
+  std::string edgesToString(EqualityEdgeId edgeId) const;
+
+  /**
+   * Map from a node to it's first edge in the equality graph. Edges are added to the front of the
+   * list which makes the insertion/backtracking easy.
+   */
+  std::vector<EqualityEdgeId> d_equalityGraph;
+
+  /** Add an edge to the equality graph */
+  void addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason);
+
+  /** Returns the equality node of the given node */
+  EqualityNode& getEqualityNode(TNode node);
+
+  /** Returns the equality node of the given node */
+  EqualityNode& getEqualityNode(EqualityNodeId nodeId);
+
+  /** Returns the id of the node */
+  EqualityNodeId getNodeId(TNode node) const;
+
+  /** Merge the class2 into class1 */
+  void merge(EqualityNode& class1, EqualityNode& class2, std::vector<TriggerId>& triggers);
+
+  /** Undo the mereg of class2 into class1 */
+  void undoMerge(EqualityNode& class1, EqualityNode& class2, EqualityNodeId class2Id);
+
+  /** Backtrack the information if necessary */
+  void backtrack();
+
+  /**
+   * Data used in the BFS search through the equality graph.
+   */
+  struct BfsData {
+    // The current node
+    EqualityNodeId nodeId;
+    // The index of the edge we traversed
+    EqualityEdgeId edgeId;
+    // Index in the queue of the previous node. Shouldn't be too much of them, at most the size
+    // of the biggest equivalence class
+    size_t previousIndex;
+
+    BfsData(EqualityNodeId nodeId = null_id, EqualityEdgeId edgeId = null_edge, size_t prev = 0)
+    : nodeId(nodeId), edgeId(edgeId), previousIndex(prev) {}
+  };
+
+  /**
+   * Trigger that will be updated
+   */
+  struct Trigger {
+    /** The current class id of the LHS of the trigger */
+    EqualityNodeId classId;
+    /** Next trigger for class 1 */
+    TriggerId nextTrigger;
+
+    Trigger(EqualityNodeId classId, TriggerId nextTrigger)
+    : classId(classId), nextTrigger(nextTrigger) {}
+  };
+
+  /**
+   * Vector of triggers (persistent and not-backtrackable). Triggers come in pairs for an
+   * equality trigger (t1, t2): one at position 2k for t1, and one at position 2k + 1 for t2. When
+   * updating triggers we always know where the other one is (^1).
+   */
+  std::vector<Trigger> d_equalityTriggers;
+
+  /**
+   * Vector of original equalities of the triggers.
+   */
+  std::vector<TNode> d_equalityTriggersOriginal;
+
+  /**
+   * Trigger lists per node. The begin id changes as we merge, but the end always points to
+   * the actual end of the triggers for this node.
+   */
+  std::vector<TriggerId> d_nodeTriggers;
+
+  /**
+   * Adds the trigger with triggerId to the beginning of the trigger list of the node with id nodeId.
+   */
+  void addTriggerToList(EqualityNodeId nodeId, TriggerId triggerId);
+
+  /** Statistics */
+  Statistics d_stats;
+
+  /** Add a new function application node to the database, i.e APP t1 t2 */
+  EqualityNodeId newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2);
+
+  /** Add a new node to the database */
+  EqualityNodeId newNode(TNode t, bool isApplication);
+
+  struct MergeCandidate {
+    EqualityNodeId t1Id, t2Id;
+    MergeReasonType type;
+    TNode reason;
+    MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason):
+      t1Id(x), t2Id(y), type(type), reason(reason) {}
+
+    std::string toString(EqualityEngine& eqEngine) const {
+      std::stringstream ss;
+      ss << eqEngine.d_nodes[t1Id] << " = " << eqEngine.d_nodes[t2Id] << ", " << type;
+      return ss.str();
+    }
+  };
+
+  /** Propagation queue */
+  std::queue<MergeCandidate> d_propagationQueue;
+
+  /** Enqueue to the propagation queue */
+  void enqueue(const MergeCandidate& candidate);
+
+  /** Do the propagation (if check is on, congruences are checked again) */
+  void propagate(bool check);
+
+  /**
+   * Get an explanation of the equality t1 = t2. Returns the asserted equalities that
+   * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
+   * else. TODO: mark the phantom equalities (skolems).
+   */
+  void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const;
+
+  /**
+   * Print the equality graph.
+   */
+  void debugPrintGraph();
+
+public:
+
+  /**
+   * Initialize the equality engine, given the owning class. This will initialize the notifier with
+   * the owner information.
+   */
+  EqualityEngine(NotifyClass& notify, context::Context* context, std::string name)
+  : d_notify(notify), d_assertedEqualitiesCount(context, 0), d_stats(name) {
+    Debug("equality") << "EqualityEdge::EqualityEngine(): id_null = " << +null_id << std::endl;
+    Debug("equality") << "EqualityEdge::EqualityEngine(): edge_null = " << +null_edge << std::endl;
+    Debug("equality") << "EqualityEdge::EqualityEngine(): trigger_null = " << +null_trigger << std::endl;
+  }
+
+  /**
+   * Adds a term to the term database.
+   */
+  void addTerm(TNode t);
+
+  /**
+   * Add a kind to treat as function applications.
+   */
+  void addFunctionKind(Kind fun) {
+    d_congruenceKinds |= fun;
+  }
+
+  /**
+   * Adds a function application term to the database.
+   */
+
+  /**
+   * Check whether the node is already in the database.
+   */
+  bool hasTerm(TNode t) const;
+
+  /**
+   * Adds an equality t1 = t2 to the database.
+   */
+  void addEquality(TNode t1, TNode t2, TNode reason);
+
+  /**
+   * Returns the representative of the term t.
+   */
+  TNode getRepresentative(TNode t) const;
+
+  /**
+   * Returns true if the two nodes are in the same class.
+   */
+  bool areEqual(TNode t1, TNode t2) const;
+
+  /**
+   * Get an explanation of the equality t1 = t2. Returns the asserted equalities that
+   * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
+   * else. TODO: mark the phantom equalities (skolems).
+   */
+  void getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const;
+
+  /**
+   * Adds a notify trigger for equality t1 = t2, i.e. when t1 = t2 the notify will be called with
+   * (t1 = t2).
+   */
+  void addTriggerEquality(TNode t1, TNode t2, TNode trigger);
+
+};
+
+} // Namespace uf
+} // Namespace theory
+} // Namespace CVC4
+
diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h
new file mode 100644
index 000000000..292761c46
--- /dev/null
+++ b/src/theory/uf/equality_engine_impl.h
@@ -0,0 +1,715 @@
+/*********************                                                        */
+/*! \file equality_engine_impl.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::enqueue(const MergeCandidate& candidate) {
+    Debug("equality") << "EqualityEngine::enqueue(" << candidate.toString(*this) << ")" << std::endl;
+    d_propagationQueue.push(candidate);
+}
+
+template <typename NotifyClass>
+EqualityNodeId EqualityEngine<NotifyClass>::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2) {
+  Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ")" << std::endl;
+
+  ++ d_stats.functionTermsCount;
+
+  // Get another id for this
+  EqualityNodeId funId = newNode(original, true);
+  FunctionApplication fun(t1, t2);
+  d_applications[funId] = fun;
+
+  // The function application we're creating
+  EqualityNodeId t1ClassId = getEqualityNode(t1).getFind();
+  EqualityNodeId t2ClassId = getEqualityNode(t2).getFind();
+  FunctionApplication funNormalized(t1ClassId, t2ClassId);
+
+  // Add the lookup data, if it's not already there
+  typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
+  if (find == d_applicationLookup.end()) {
+    // When we backtrack, if the lookup is not there anymore, we'll add it again
+    Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): no lookup, setting up" << std::endl;
+    d_applicationLookup[funNormalized] = funId;
+  } else {
+    // If it's there, we need to merge these two
+    Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): lookup exists, adding to queue" << std::endl;
+    enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null()));
+    propagate(false);
+  }
+
+  // Add to the use lists
+  d_equalityNodes[t1].usedIn(funId, d_useListNodes);
+  d_equalityNodes[t2].usedIn(funId, d_useListNodes);
+
+  // Return the new id
+  Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ") => " << funId << std::endl;
+
+  return funId;
+}
+
+template <typename NotifyClass>
+EqualityNodeId EqualityEngine<NotifyClass>::newNode(TNode node, bool isApplication) {
+
+  Debug("equality") << "EqualityEngine::newNode(" << node << ", " << (isApplication ? "function" : "regular") << ")" << std::endl;
+
+  ++ d_stats.termsCount;
+
+  // Register the new id of the term
+  EqualityNodeId newId = d_nodes.size();
+  d_nodeIds[node] = newId;
+  // Add the node to it's position
+  d_nodes.push_back(node);
+  // Note if this is an application or not
+  d_applications.push_back(FunctionApplication());
+  // Add the trigger list for this node
+  d_nodeTriggers.push_back(+null_trigger);
+  // Add it to the equality graph
+  d_equalityGraph.push_back(+null_edge);
+  // Add the equality node to the nodes
+  d_equalityNodes.push_back(EqualityNode(newId));
+
+  Debug("equality") << "EqualityEngine::newNode(" << node << ", " << (isApplication ? "function" : "regular") << ") => " << newId << std::endl;
+
+  return newId;
+}
+
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addTerm(TNode t) {
+
+  Debug("equality") << "EqualityEngine::addTerm(" << t << ")" << std::endl;
+
+  // If there already, we're done
+  if (hasTerm(t)) {
+    return;
+  }
+
+  EqualityNodeId result;
+
+  // If a function application we go in
+  if (t.getNumChildren() > 0 && d_congruenceKinds[t.getKind()])
+  {
+    // Add the operator
+    TNode tOp = t.getOperator();
+    addTerm(tOp);
+    // Add all the children and Curryfy
+    result = getNodeId(tOp);
+    for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
+      // Add the child
+      addTerm(t[i]);
+      // Add the application
+      result = newApplicationNode(t, result, getNodeId(t[i]));
+    }
+  } else {
+    // Otherwise we just create the new id
+    result = newNode(t, false);
+  }
+
+  Debug("equality") << "EqualityEngine::addTerm(" << t << ") => " << result << std::endl;
+}
+
+template <typename NotifyClass>
+bool EqualityEngine<NotifyClass>::hasTerm(TNode t) const {
+  return d_nodeIds.find(t) != d_nodeIds.end();
+}
+
+template <typename NotifyClass>
+EqualityNodeId EqualityEngine<NotifyClass>::getNodeId(TNode node) const {
+  Assert(hasTerm(node), node.toString().c_str());
+  return (*d_nodeIds.find(node)).second;
+}
+
+template <typename NotifyClass>
+EqualityNode& EqualityEngine<NotifyClass>::getEqualityNode(TNode t) {
+  return getEqualityNode(getNodeId(t));
+}
+
+template <typename NotifyClass>
+EqualityNode& EqualityEngine<NotifyClass>::getEqualityNode(EqualityNodeId nodeId) {
+  Assert(nodeId < d_equalityNodes.size());
+  return d_equalityNodes[nodeId];
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addEquality(TNode t1, TNode t2, TNode reason) {
+
+  Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl;
+
+  // Backtrack if necessary
+  backtrack();
+
+  // Add the terms if they are not already in the database
+  EqualityNodeId t1Id = getNodeId(t1);
+  EqualityNodeId t2Id = getNodeId(t2);
+
+  // Add to the queue and propagate
+  enqueue(MergeCandidate(t1Id, t2Id, MERGED_THROUGH_EQUALITY, reason));
+  propagate(false);
+}
+
+template <typename NotifyClass>
+TNode EqualityEngine<NotifyClass>::getRepresentative(TNode t) const {
+
+  Debug("equality") << "EqualityEngine::getRepresentative(" << t << ")" << std::endl;
+
+  Assert(hasTerm(t));
+
+  // Both following commands are semantically const
+  const_cast<EqualityEngine*>(this)->backtrack();
+  EqualityNodeId representativeId = const_cast<EqualityEngine*>(this)->getEqualityNode(t).getFind();
+
+  Debug("equality") << "EqualityEngine::getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl;
+
+  return d_nodes[representativeId];
+}
+
+template <typename NotifyClass>
+bool EqualityEngine<NotifyClass>::areEqual(TNode t1, TNode t2) const {
+  Debug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ")" << std::endl;
+
+  Assert(hasTerm(t1));
+  Assert(hasTerm(t2));
+
+  // Both following commands are semantically const
+  const_cast<EqualityEngine*>(this)->backtrack();
+  EqualityNodeId rep1 = const_cast<EqualityEngine*>(this)->getEqualityNode(t1).getFind();
+  EqualityNodeId rep2 = const_cast<EqualityEngine*>(this)->getEqualityNode(t2).getFind();
+
+  Debug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ") => " << (rep1 == rep2 ? "true" : "false") << std::endl;
+
+  return rep1 == rep2;
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::merge(EqualityNode& class1, EqualityNode& class2, std::vector<TriggerId>& triggers) {
+
+  Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl;
+
+  Assert(triggers.empty());
+
+  ++ d_stats.mergesCount;
+
+  EqualityNodeId class1Id = class1.getFind();
+  EqualityNodeId class2Id = class2.getFind();
+
+  // Update class2 representative information
+  Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating class " << class2Id << std::endl;
+  EqualityNodeId currentId = class2Id;
+  do {
+    // Get the current node
+    EqualityNode& currentNode = getEqualityNode(currentId);
+
+    // Update it's find to class1 id
+    Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << "->" << class1Id << std::endl;
+    currentNode.setFind(class1Id);
+
+    // Go through the triggers and inform if necessary
+    TriggerId currentTrigger = d_nodeTriggers[currentId];
+    while (currentTrigger != null_trigger) {
+      Trigger& trigger = d_equalityTriggers[currentTrigger];
+      Trigger& otherTrigger = d_equalityTriggers[currentTrigger ^ 1];
+
+      // If the two are not already in the same class
+      if (otherTrigger.classId != trigger.classId) {
+        trigger.classId = class1Id;
+        // If they became the same, call the trigger
+        if (otherTrigger.classId == class1Id) {
+          // Id of the real trigger is half the internal one
+          triggers.push_back(currentTrigger);
+        }
+      }
+
+      // Go to the next trigger
+      currentTrigger = trigger.nextTrigger;
+    }
+
+    // Move to the next node
+    currentId = currentNode.getNext();
+
+  } while (currentId != class2Id);
+
+
+  // Update class2 table lookup and information
+  Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl;
+  do {
+    // Get the current node
+    EqualityNode& currentNode = getEqualityNode(currentId);    
+    Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl;
+ 
+    // Go through the uselist and check for congruences
+    UseListNodeId currentUseId = currentNode.getUseList();
+    while (currentUseId != null_uselist_id) {
+      // Get the node of the use list
+      UseListNode& useNode = d_useListNodes[currentUseId];
+      // Get the function application
+      EqualityNodeId funId = useNode.getApplicationId();
+      Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << " in " << d_nodes[funId] << std::endl;
+      const FunctionApplication& fun = d_applications[useNode.getApplicationId()];
+      // Check if there is an application with find arguments
+      EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
+      EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind();
+      FunctionApplication funNormalized(aNormalized, bNormalized);
+      typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
+      if (find != d_applicationLookup.end()) {
+        // Applications fun and the funNormalized can be merged due to congruence
+        if (getEqualityNode(funId).getFind() != getEqualityNode(find->second).getFind()) {
+          enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null()));
+        }
+      } else {
+        // There is no representative, so we can add one, we remove this when backtracking
+        d_applicationLookup[funNormalized] = funId;
+      }
+      // Go to the next one in the use list
+      currentUseId = useNode.getNext();
+    }
+
+    // Move to the next node
+    currentId = currentNode.getNext();
+  } while (currentId != class2Id);
+
+  // Now merge the lists
+  class1.merge<true>(class2);
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::undoMerge(EqualityNode& class1, EqualityNode& class2, EqualityNodeId class2Id) {
+
+  Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << ")" << std::endl;
+
+  // Now unmerge the lists (same as merge)
+  class1.merge<false>(class2);
+
+  // First undo the table lookup changes
+  Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << "): undoing lookup changes" << std::endl;
+  EqualityNodeId currentId = class2Id;
+  do {
+    // Get the current node
+    EqualityNode& currentNode = getEqualityNode(currentId);
+
+    // Go through the uselist and check for congruences
+    UseListNodeId currentUseId = currentNode.getUseList();
+    while (currentUseId != null_uselist_id) {
+      // Get the node of the use list
+      UseListNode& useNode = d_useListNodes[currentUseId];
+      // Get the function application
+      EqualityNodeId funId = useNode.getApplicationId();
+      const FunctionApplication& fun = d_applications[useNode.getApplicationId()];
+      // Get the application with find arguments
+      EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
+      EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind();
+      FunctionApplication funNormalized(aNormalized, bNormalized);
+      typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
+      // If the id is the one we set, then we undo it
+      if (find != d_applicationLookup.end() && find->second == funId) {
+        d_applicationLookup.erase(find);
+      }
+      // Go to the next one in the use list
+      currentUseId = useNode.getNext();
+    }
+
+    // Move to the next node
+    currentId = currentNode.getNext();
+
+  } while (currentId != class2Id);
+
+  // Update class2 representative information
+  Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << "): undoing representative info" << std::endl;
+  do {
+    // Get the current node
+    EqualityNode& currentNode = getEqualityNode(currentId);
+
+    // Update it's find to class1 id
+    currentNode.setFind(class2Id);
+
+    // Go through the trigger list (if any) and undo the class
+    TriggerId currentTrigger = d_nodeTriggers[currentId];
+    while (currentTrigger != null_trigger) {
+      Trigger& trigger = d_equalityTriggers[currentTrigger];
+      trigger.classId = class2Id;
+      currentTrigger = trigger.nextTrigger;
+    }
+
+    // Move to the next node
+    currentId = currentNode.getNext();
+
+  } while (currentId != class2Id);
+
+  // Now set any missing lookups and check for any congruences on backtrack
+  std::vector<MergeCandidate> possibleCongruences;
+  Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << "): checking for any unset lookups" << std::endl;
+  do {
+    // Get the current node
+    EqualityNode& currentNode = getEqualityNode(currentId);
+
+    // Go through the uselist and check for congruences
+    UseListNodeId currentUseId = currentNode.getUseList();
+    while (currentUseId != null_uselist_id) {
+      // Get the node of the use list
+      UseListNode& useNode = d_useListNodes[currentUseId];
+      // Get the function application
+      EqualityNodeId funId = useNode.getApplicationId();
+      const FunctionApplication& fun = d_applications[useNode.getApplicationId()];
+      // Get the application with find arguments
+      EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
+      EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind();
+      FunctionApplication funNormalized(aNormalized, bNormalized);
+      typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
+      Assert(find != d_applicationLookup.end());
+      // If the id doesn't exist, we'll set it
+      if (find == d_applicationLookup.end()) {
+        d_applicationLookup[funNormalized] = funId;
+      } else {
+        // Otherwise, we might be congruent agaain
+        if (getEqualityNode(funId).getFind() != getEqualityNode(find->second).getFind()) {
+          // Damn, we might be merging again, but we'll check this later
+          enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null()));
+        }
+      }
+      // Go to the next one in the use list
+      currentUseId = useNode.getNext();
+    }
+
+    // Move to the next node
+    currentId = currentNode.getNext();
+
+  } while (currentId != class2Id);
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::backtrack() {
+
+  // If we need to backtrack then do it
+  if (d_assertedEqualitiesCount < d_assertedEqualities.size()) {
+
+    // Clear the propagation queue
+    while (!d_propagationQueue.empty()) {
+      d_propagationQueue.pop();
+    }
+
+    ++ d_stats.backtracksCount;
+
+    Debug("equality") << "EqualityEngine::backtrack(): nodes" << std::endl;
+
+    for (int i = (int)d_assertedEqualities.size() - 1, i_end = (int)d_assertedEqualitiesCount; i >= i_end; --i) {
+      // Get the ids of the merged classes
+      Equality& eq = d_assertedEqualities[i];
+      // Undo the merge
+      undoMerge(d_equalityNodes[eq.lhs], d_equalityNodes[eq.rhs], eq.rhs);
+    }
+
+    d_assertedEqualities.resize(d_assertedEqualitiesCount);
+
+    Debug("equality") << "EqualityEngine::backtrack(): edges" << std::endl;
+
+    for (int i = (int)d_equalityEdges.size() - 2, i_end = (int)(2*d_assertedEqualitiesCount); i >= i_end; i -= 2) {
+      EqualityEdge& edge1 = d_equalityEdges[i];
+      EqualityEdge& edge2 = d_equalityEdges[i | 1];
+      d_equalityGraph[edge2.getNodeId()] = edge1.getNext();
+      d_equalityGraph[edge1.getNodeId()] = edge2.getNext();
+    }
+
+    d_equalityEdges.resize(2 * d_assertedEqualitiesCount);
+
+    // Now repropagate if something got reenqueued
+    propagate(true);
+  }
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) {
+  Debug("equality") << "EqualityEngine::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << "," << reason << ")" << std::endl;
+  EqualityEdgeId edge = d_equalityEdges.size();
+  d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1], type, reason));
+  d_equalityEdges.push_back(EqualityEdge(t1, d_equalityGraph[t2], type, reason));
+  d_equalityGraph[t1] = edge;
+  d_equalityGraph[t2] = edge | 1;
+
+  if (Debug.isOn("equality::internal")) {
+    const_cast<EqualityEngine*>(this)->debugPrintGraph();
+  }
+}
+
+template <typename NotifyClass>
+std::string EqualityEngine<NotifyClass>::edgesToString(EqualityEdgeId edgeId) const {
+  std::stringstream out;
+  bool first = true;
+  if (edgeId == null_edge) {
+    out << "null";
+  } else {
+    while (edgeId != null_edge) {
+      const EqualityEdge& edge = d_equalityEdges[edgeId];
+      if (!first) out << ",";
+      out << d_nodes[edge.getNodeId()];
+      edgeId = edge.getNext();
+      first = false;
+    }
+  }
+  return out.str();
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const {
+  Assert(getRepresentative(t1) == getRepresentative(t2));
+
+  Debug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl;
+
+  // Backtrack if necessary
+  const_cast<EqualityEngine*>(this)->backtrack();
+
+  // Get the explanation
+  EqualityNodeId t1Id = getNodeId(t1);
+  EqualityNodeId t2Id = getNodeId(t2);
+  getExplanation(t1Id, t2Id, equalities);
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const {
+
+  Debug("equality") << "EqualityEngine::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl;
+
+  // If the nodes are the same, we're done
+  if (t1Id == t2Id) return;
+
+  if (Debug.isOn("equality::internal")) {
+    const_cast<EqualityEngine*>(this)->debugPrintGraph();
+  }
+
+  // Queue for the BFS containing nodes
+  std::vector<BfsData> bfsQueue;
+
+  // Find a path from t1 to t2 in the graph (BFS)
+  bfsQueue.push_back(BfsData(t1Id, null_id, 0));
+  size_t currentIndex = 0;
+  while (true) {
+    // There should always be a path, and every node can be visited only once (tree)
+    Assert(currentIndex < bfsQueue.size());
+
+    // The next node to visit
+    BfsData current = bfsQueue[currentIndex];
+    EqualityNodeId currentNode = current.nodeId;
+
+    Debug("equality") << "EqualityEngine::getExplanation(): currentNode =  " << d_nodes[currentNode] << std::endl;
+
+    // Go through the equality edges of this node
+    EqualityEdgeId currentEdge = d_equalityGraph[currentNode];
+    Debug("equality") << "EqualityEngine::getExplanation(): edgesId =  " << currentEdge << std::endl;
+    Debug("equality") << "EqualityEngine::getExplanation(): edges =  " << edgesToString(currentEdge) << std::endl;
+
+    while (currentEdge != null_edge) {
+      // Get the edge
+      const EqualityEdge& edge = d_equalityEdges[currentEdge];
+
+      // If not just the backwards edge
+      if ((currentEdge | 1u) != (current.edgeId | 1u)) {
+
+        Debug("equality") << "EqualityEngine::getExplanation(): currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
+
+        // Did we find the path
+        if (edge.getNodeId() == t2Id) {
+
+          Debug("equality") << "EqualityEngine::getExplanation(): path found: " << std::endl;
+
+          // Reconstruct the path
+          do {
+            // The current node
+            currentNode = bfsQueue[currentIndex].nodeId;
+            EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId();
+            MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType();
+
+            Debug("equality") << "EqualityEngine::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl;
+
+            // Add the actual equality to the vector
+            if (reasonType == MERGED_THROUGH_CONGRUENCE) {
+              // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2
+              Debug("equality") << "EqualityEngine::getExplanation(): due to congruence, going deeper" << std::endl;
+              const FunctionApplication& f1 = d_applications[currentNode];
+              const FunctionApplication& f2 = d_applications[edgeNode];
+              Debug("equality") << push;
+              getExplanation(f1.a, f2.a, equalities);
+              getExplanation(f1.b, f2.b, equalities);
+              Debug("equality") << pop;
+            } else {
+              // Construct the equality
+              Debug("equality") << "EqualityEngine::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl;
+              equalities.push_back(d_equalityEdges[currentEdge].getReason());
+            }
+
+            // Go to the previous
+            currentEdge = bfsQueue[currentIndex].edgeId;
+            currentIndex = bfsQueue[currentIndex].previousIndex;
+          } while (currentEdge != null_id);
+
+          // Done
+          return;
+        }
+
+        // Push to the visitation queue if it's not the backward edge
+        bfsQueue.push_back(BfsData(edge.getNodeId(), currentEdge, currentIndex));
+      }
+
+      // Go to the next edge
+      currentEdge = edge.getNext();
+    }
+
+    // Go to the next node to visit
+    ++ currentIndex;
+  }
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addTriggerEquality(TNode t1, TNode t2, TNode trigger) {
+
+  Debug("equality") << "EqualityEngine::addTrigger(" << t1 << ", " << t2 << ", " << trigger << ")" << std::endl;
+
+  Assert(hasTerm(t1));
+  Assert(hasTerm(t2));
+
+  // Get the information about t1
+  EqualityNodeId t1Id = getNodeId(t1);
+  EqualityNodeId t1classId = getEqualityNode(t1Id).getFind();
+  TriggerId t1TriggerId = d_nodeTriggers[t1Id];
+
+  // Get the information about t2
+  EqualityNodeId t2Id = getNodeId(t2);
+  EqualityNodeId t2classId = getEqualityNode(t2Id).getFind();
+  TriggerId t2TriggerId = d_nodeTriggers[t2Id];
+
+  Debug("equality") << "EqualityEngine::addTrigger(" << trigger << "): " << t1Id << " (" << t1classId << ") = " << t2Id << " (" << t2classId << ")" << std::endl;
+
+  // Create the triggers
+  TriggerId t1NewTriggerId = d_equalityTriggers.size();
+  TriggerId t2NewTriggerId = t1NewTriggerId | 1;
+  d_equalityTriggers.push_back(Trigger(t1classId, t1TriggerId));
+  d_equalityTriggersOriginal.push_back(trigger);
+  d_equalityTriggers.push_back(Trigger(t2classId, t2TriggerId));
+  d_equalityTriggersOriginal.push_back(trigger);
+
+  // Add the trigger to the trigger graph
+  d_nodeTriggers[t1Id] = t1NewTriggerId;
+  d_nodeTriggers[t2Id] = t2NewTriggerId;
+
+  // If the trigger is already on, we propagate
+  if (t1classId == t2classId) {
+    Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << "): triggered at setup time" << std::endl;
+    d_notify.notifyEquality(trigger); // Don't care about the return value
+  }
+
+  Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl;
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::propagate(bool check) {
+
+  Debug("equality") << "EqualityEngine::propagate()" << std::endl;
+
+  bool done = false;
+  while (!d_propagationQueue.empty()) {
+
+    // The current merge candidate
+    const MergeCandidate current = d_propagationQueue.front();
+    d_propagationQueue.pop();
+
+    if (done) {
+      // If we're done, just empty the queue
+      continue;
+    }
+
+    // Get the representatives
+    EqualityNodeId t1classId = getEqualityNode(current.t1Id).getFind();
+    EqualityNodeId t2classId = getEqualityNode(current.t2Id).getFind();
+
+    // If already the same, we're done
+    if (t1classId == t2classId) {
+      continue;
+    }
+
+    // If check is on, and a congruence, check the arguments (it might be from a backtrack)
+    if (check && current.type == MERGED_THROUGH_CONGRUENCE) {
+      const FunctionApplication& f1 = d_applications[current.t1Id];
+      const FunctionApplication& f2 = d_applications[current.t2Id];
+      if (getEqualityNode(f1.a).getFind() != getEqualityNode(f2.a).getFind()) continue;
+      if (getEqualityNode(f1.b).getFind() != getEqualityNode(f2.b).getFind()) continue;
+    }
+
+    // Get the nodes of the representatives
+    EqualityNode& node1 = getEqualityNode(t1classId);
+    EqualityNode& node2 = getEqualityNode(t2classId);
+
+    Assert(node1.getFind() == t1classId);
+    Assert(node2.getFind() == t2classId);
+
+    // Depending on the merge preference (such as size), merge them
+    std::vector<TriggerId> triggers;
+    if (node2.getSize() > node1.getSize()) {
+      Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl;
+      merge(node2, node1, triggers);
+      d_assertedEqualities.push_back(Equality(t2classId, t1classId));
+    } else {
+      Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t2Id] << " into " << d_nodes[current.t1Id] << std::endl;
+      merge(node1, node2, triggers);
+      d_assertedEqualities.push_back(Equality(t1classId, t2classId));
+    }
+
+    // Add the actuall equality to the equality graph
+    addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason);
+
+    // One more equality added
+    d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
+
+    Assert(2*d_assertedEqualities.size() == d_equalityEdges.size());
+    Assert(d_assertedEqualities.size() == d_assertedEqualitiesCount);
+
+    // Notify the triggers
+    for (size_t trigger = 0, trigger_end = triggers.size(); trigger < trigger_end && !done; ++ trigger) {
+      // Notify the trigger and exit if it fails
+      done = !d_notify.notifyEquality(d_equalityTriggersOriginal[triggers[trigger]]);
+    }
+  }
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::debugPrintGraph() {
+  for (EqualityNodeId nodeId = 0; nodeId < d_nodes.size(); ++ nodeId) {
+
+    Debug("equality::internal") << d_nodes[nodeId] << " " << nodeId << "(" << getEqualityNode(nodeId).getFind() << "):";
+
+    EqualityEdgeId edgeId = d_equalityGraph[nodeId];
+    while (edgeId != null_edge) {
+      const EqualityEdge& edge = d_equalityEdges[edgeId];
+      Debug("equality::internal") << " " << d_nodes[edge.getNodeId()] << ":" << edge.getReason();
+      edgeId = edge.getNext();
+    }
+
+    Debug("equality::internal") << std::endl;
+  }
+}
+
+} // Namespace uf
+} // Namespace theory
+} // Namespace CVC4
+
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
new file mode 100644
index 000000000..0571126e6
--- /dev/null
+++ b/src/theory/uf/theory_uf.cpp
@@ -0,0 +1,214 @@
+/*********************                                                        */
+/*! \file theory_uf.cpp
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is the interface to TheoryUF implementations
+ **
+ ** This is the interface to TheoryUF implementations.  All
+ ** implementations of TheoryUF should inherit from this class.
+ **/
+
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/equality_engine_impl.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+
+using namespace std;
+
+Node mkAnd(const std::vector<TNode>& conjunctions) {
+  Assert(conjunctions.size() > 0);
+
+  std::set<TNode> all;
+  all.insert(conjunctions.begin(), conjunctions.end());
+
+  if (all.size() == 1) {
+    // All the same, or just one
+    return conjunctions[0];
+  }
+
+  NodeBuilder<> conjunction(kind::AND);
+  std::set<TNode>::const_iterator it = all.begin();
+  std::set<TNode>::const_iterator it_end = all.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
+  }
+
+  return conjunction;
+}
+
+void TheoryUF::check(Effort level) {
+
+  while (!done() && !d_conflict) {
+    // Get all the assertions
+    TNode assertion = get();
+    Debug("uf") << "TheoryUF::check(): processing " << assertion << std::endl;
+
+    // Fo the work
+    switch (assertion.getKind()) {
+    case kind::EQUAL:
+      d_equalityEngine.addEquality(assertion[0], assertion[1], assertion);
+      break;
+    case kind::APPLY_UF:
+      d_equalityEngine.addEquality(assertion, d_true, assertion);
+    case kind::NOT:
+      if (assertion[0].getKind() == kind::APPLY_UF) {
+        d_equalityEngine.addEquality(assertion[0], d_false, assertion);
+      }
+      break;
+    default:
+      Unreachable();
+    }
+  }
+
+  // If in conflict, output the conflict
+  if (d_conflict) {
+    Debug("uf") << "TheoryUF::check(): conflict " << d_conflictNode << std::endl;
+    d_out->conflict(d_conflictNode);
+    d_literalsToPropagate.clear();
+  }
+
+  // Otherwise we propagate in order to detect a weird conflict like
+  // p, x = y
+  // p -> f(x) != f(y) -- f(x) = f(y) gets added to the propagation list at preregistration time
+  // but when f(x) != f(y) is deduced by the sat solver, so it's asserted, and we don't detect the conflict
+  // until we go through the propagation list
+  propagate(level);
+}
+
+void TheoryUF::propagate(Effort level) {
+  Debug("uf") << "TheoryUF::propagate()" << std::endl;
+  if (!d_conflict) {
+    for (unsigned i = 0; i < d_literalsToPropagate.size(); ++ i) {
+      TNode literal = d_literalsToPropagate[i];
+      Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl;
+      bool satValue;
+      if (!d_valuation.hasSatValue(literal, satValue)) {
+        d_out->propagate(literal);
+      } else {
+        std::vector<TNode> assumptions;
+        if (literal != d_false) {
+          TNode negatedLiteral = literal.getKind() == kind::NOT ? literal[0] : (TNode) literal.notNode();
+          assumptions.push_back(negatedLiteral);
+        }
+        explain(literal, assumptions);
+        d_conflictNode = mkAnd(assumptions);
+        d_conflict = true;
+        break;
+      }
+    }
+  }
+  d_literalsToPropagate.clear();
+}
+
+void TheoryUF::preRegisterTerm(TNode node) {
+  Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl;
+
+  switch (node.getKind()) {
+  case kind::EQUAL:
+    // Add the terms
+    d_equalityEngine.addTerm(node[0]);
+    d_equalityEngine.addTerm(node[1]);
+    // Add the trigger
+    d_equalityEngine.addTriggerEquality(node[0], node[1], node);
+    break;
+  case kind::APPLY_UF:
+    // Function applications/predicates
+    d_equalityEngine.addTerm(node);
+    // Maybe it's a predicate
+    if (node.getType().isBoolean()) {
+      // Get triggered for both equal and dis-equal
+      d_equalityEngine.addTriggerEquality(node, d_true, node);
+      d_equalityEngine.addTriggerEquality(node, d_false, node.notNode());
+    }
+  default:
+    // Variables etc
+    d_equalityEngine.addTerm(node);
+    break;
+  }
+}
+
+bool TheoryUF::propagate(TNode atom, bool isTrue) {
+  Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ")" << std::endl;
+
+  // If already in conflict, no more propagation
+  if (d_conflict) {
+    Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << "): already in conflict" << std::endl;
+    return false;
+  }
+
+  // The literal
+  TNode literal = isTrue ? (Node) atom : atom.notNode();
+
+  // See if the literal has been asserted already
+  bool satValue = false;
+  bool isAsserted = literal == d_false || d_valuation.hasSatValue(literal, satValue);
+
+  // If asserted, we're done or in conflict
+  if (isAsserted) {
+    if (satValue) {
+      Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ") => already known" << std::endl;
+      return true;
+    } else {
+      Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ") => conflict" << std::endl;
+      std::vector<TNode> assumptions;
+      if (literal != d_false) {
+        TNode negatedLiteral = isTrue ? atom.notNode() : (Node) atom;
+        assumptions.push_back(negatedLiteral);
+      }
+      explain(literal, assumptions);
+      d_conflictNode = mkAnd(assumptions);
+      d_conflict = true;
+      return false;
+    }
+  }
+
+  // Nothing, just enqueue it for propagation and mark it as asserted already
+  Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ") => enqueuing for propagation" << std::endl;
+  d_literalsToPropagate.push_back(literal);
+
+  return true;
+}
+
+void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
+  TNode lhs, rhs;
+  switch (literal.getKind()) {
+    case kind::EQUAL:
+      lhs = literal[0];
+      rhs = literal[1];
+      break;
+    case kind::APPLY_UF:
+      lhs = literal;
+      rhs = d_true;
+      break;
+    case kind::NOT:
+      lhs = literal[0];
+      rhs = d_false;
+    case kind::CONST_BOOLEAN:
+      // we get to explain true = false, since we set false to be the trigger of this
+      lhs = d_true;
+      rhs = d_false;
+      break;
+    default:
+      Unreachable();
+  }
+  d_equalityEngine.getExplanation(lhs, rhs, assumptions);
+}
+
+void TheoryUF::explain(TNode literal) {
+  Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
+  std::vector<TNode> assumptions;
+  explain(literal, assumptions);
+  d_out->explanation(mkAnd(assumptions));
+}
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 34d6df881..266a1b7b4 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /*! \file theory_uf.h
  ** \verbatim
- ** Original author: mdeters
+ ** Original author: dejan
  ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
@@ -26,28 +26,97 @@
 #include "expr/attribute.h"
 
 #include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
 
-#include "context/context.h"
+#include "context/cdo.h"
+#include "context/cdset.h"
 
 namespace CVC4 {
 namespace theory {
 namespace uf {
 
 class TheoryUF : public Theory {
+
+public:
+
+  class NotifyClass {
+    TheoryUF& d_uf;
+  public:
+    NotifyClass(TheoryUF& uf): d_uf(uf) {}
+
+    bool notifyEquality(TNode eq) {
+      Debug("uf") << "NotifyClass::notifyEquality(" << eq << ")" << std::endl;
+      // Just forward to uf
+      return d_uf.propagate(eq, true);
+    }
+  };
+
+private:
+
+  /** The notify class */
+  NotifyClass d_notify;
+
+  /** Equaltity engine */
+  EqualityEngine<NotifyClass> d_equalityEngine;
+
+  /** All the literals known to be true */
+  context::CDSet<TNode, TNodeHashFunction> d_knownFacts;
+
+  /** Are we in conflict */
+  context::CDO<bool> d_conflict;
+
+  /** The conflict node */
+  Node d_conflictNode;
+
+  /**
+   * Should be called to propagate the atom. If isTrue is true, the atom should be propagated,
+   * otherwise the negated atom should be propagated.
+   */
+  bool propagate(TNode atom, bool isTrue);
+
+  /**
+   * Explain why this literal is true by adding assumptions
+   */
+  void explain(TNode literal, std::vector<TNode>& assumptions);
+
+  /** Literals to propagate */
+  std::vector<TNode> d_literalsToPropagate;
+
+  /** True node for predicates = true */
+  Node d_true;
+
+  /** True node for predicates = false */
+  Node d_false;
+
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUF(context::Context* ctxt, OutputChannel& out, Valuation valuation)
-    : Theory(THEORY_UF, ctxt, out, valuation) { }
-
-  // We declare these here (even though it's not terribly useful) for
-  // documentation reasons, and to keep mktheorytraits from issuing a
-  // spurious warning.
-  virtual void check(Effort) = 0;
-  virtual void propagate(Effort) {}
-  virtual void staticLearning(TNode in, NodeBuilder<>& learned) {}
-  virtual void notifyRestart() {}
-  virtual void presolve() {}
+  TheoryUF(context::Context* ctxt, OutputChannel& out, Valuation valuation):
+    Theory(THEORY_UF, ctxt, out, valuation),
+    d_notify(*this),
+    d_equalityEngine(d_notify, ctxt, "theory::uf::TheoryUF"),
+    d_knownFacts(ctxt),
+    d_conflict(ctxt, false)
+  {
+    // The kinds we are treating as function application in congruence
+    d_equalityEngine.addFunctionKind(kind::APPLY_UF);
+
+    // The boolean constants
+    d_true = NodeManager::currentNM()->mkConst<bool>(true);
+    d_false = NodeManager::currentNM()->mkConst<bool>(false);
+    d_equalityEngine.addTerm(d_true);
+    d_equalityEngine.addTerm(d_false);
+    d_equalityEngine.addTriggerEquality(d_true, d_false, d_false);
+  }
+
+  void check(Effort);
+  void propagate(Effort);
+  void preRegisterTerm(TNode term);
+  void explain(TNode n);
+
+  std::string identify() const {
+    return "THEORY_UF";
+  }
 
 };/* class TheoryUF */
 
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 536255c2d..0aefd7f21 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -27,6 +27,10 @@ Node Valuation::getValue(TNode n) const {
   return d_engine->getValue(n);
 }
 
+bool Valuation::hasSatValue(TNode n, bool& value) const {
+  return d_engine->getPropEngine()->hasValue(n, value);
+}
+
 Node Valuation::getSatValue(TNode n) const{
   if(n.getKind() == kind::NOT) {
     Node atomRes = d_engine->getPropEngine()->getValue(n[0]);
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 2346b6d32..ea6772ce8 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -51,6 +51,11 @@ public:
    */
   Node getSatValue(TNode n) const;
 
+  /**
+   * Returns true if the node has a sat value. If yes value is set to it's value.
+   */
+  bool hasSatValue(TNode n, bool& value) const;
+
 };/* class Valuation */
 
 }/* CVC4::theory namespace */
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index 01eaee999..45cf22232 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -19,7 +19,6 @@ TESTS =	\
 	eq_diamond1.smt \
 	eq_diamond14.reduced.smt \
 	eq_diamond14.reduced2.smt \
-	eq_diamond23.smt \
 	NEQ016_size5_reduced2a.smt \
 	NEQ016_size5_reduced2b.smt \
 	dead_dnd002.smt \