--- a/src/lite/BDDSolver.java	Thu Jan 10 02:29:42 2008 +0900
+++ b/src/lite/BDDSolver.java	Thu Jan 10 02:29:46 2008 +0900
@@ -57,6 +57,10 @@
 			else return "null";
 		}
 		if (id==BDDID.BDD) {
+			if (high.id==BDDID.True&&low.id==BDDID.False)
+				return var.toString();
+			else if (high.id==BDDID.False&&low.id==BDDID.True)
+				return "~("+var+")";
 			return "("+var+"?"+high+":"+low+")";
 		}
 		return var.toString();

--- a/src/lite/ExistsSolver.java	Thu Jan 10 02:29:42 2008 +0900
+++ b/src/lite/ExistsSolver.java	Thu Jan 10 02:29:46 2008 +0900
@@ -27,12 +27,14 @@
 
 	@Override
 	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
+		boolean old = var.value;
 		makeLocal(sat);
 		var.setValue(true);
 		try {
 			return node.sat(sat, new Continuation(sat,next,this));
 		} catch (Backtrack e) {
 			restoreLocal(sat);
+			var.setValue(old);
 			throw sat.backtrack;
 		}
 	}
@@ -55,12 +57,13 @@
 		}
 	}
 
-	private ITLSolver restoreLocal(ITLSatisfier sat,ITLSolver value,Continuation next) throws Backtrack {
+	private ITLSolver restoreLocal(ITLSatisfier sat,boolean now,ITLSolver value,Continuation next) throws Backtrack {
 		restoreLocal(sat);
 		try {
 			return next.sat(value);
 		} catch (Backtrack e) {
 			makeLocal(sat);
+			var.setValue(now);
 			throw sat.backtrack;
 		}
 	}
@@ -71,7 +74,7 @@
 			var.setValue(false);
 			return node.sat(sat, new Continuation(sat,next ,new ExistsSolver3()));
 		} else if (value==sat.true_) {
-			return restoreLocal(sat,value,next);
+			return restoreLocal(sat,var.value,value,next);
 		} else {
 			var.setValue(false);
 			residue = value;
@@ -83,18 +86,28 @@
 	class ExistsSolver2 implements Next {
 		public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
 			if (value==null) {
-				value = residue;
+				value = sat.lf.existsNode(var,residue);
 			} else if (value==sat.true_) {
 			} else {
-				value = sat.lf.existsNode(var,sat.lf.orNode(residue,value));
+				value = sat.lf.orNode(residue,value);
+				if (value==sat.true_)  {
+				} else {
+					value = sat.lf.existsNode(var,value);
+				}
 			}
-			return restoreLocal(sat,value,next);
+			return restoreLocal(sat,var.value,value,next);
 		}
 	}
+	
 	class ExistsSolver3 implements Next {
 
 		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
-			return restoreLocal(sat,value,next);
+			if (value==null) {
+			} else if (value==sat.true_) {
+			} else {
+				value = sat.lf.existsNode(var, value);
+			}
+			return restoreLocal(sat,var.value,value,next);
 		}
 	}