Merge remote-tracking branch 'refs/remotes/origin/master'

Author: muhos

src/gpu/assume.cpp

@@ -234,7 +234,6 @@ void Solver::iunassume()
 {
     assert(sp);
 	assert(inf.maxVar);
-	assert(stats.clauses.original);
 	LOGN2(2, " Resetting %d assumptions and solver state..", assumptions.size());
 	if (assumptions.size()) {
 		forall_clause(assumptions, k) {

src/gpu/solverinc.cpp

@@ -69,11 +69,6 @@ void Solver::isolve(Lits_t& assumptions)
 {
 	FAULT_DETECTOR;
 	LOGHEADER(1, 5, "Search");
-	if (!stats.clauses.original) {
-		assert(orgs.empty());
-		LOGWARNING("Formula is already SATISFIABLE by elimination");
-		return;
-	}
 	timer.start();
 	iallocspace();
 	iunassume();
@@ -82,6 +77,11 @@ void Solver::isolve(Lits_t& assumptions)
 		LOG2(2, " Incremental formula has a contradiction on top level");
 		learnEmpty();
 	}
+	else if (!stats.clauses.original) {
+		assert(orgs.empty());
+		LOG2(2, " Formula is already SATISFIABLE by elimination");
+		cnfstate = SAT;
+	}
 	else {
 		initLimits();
 		iassume(assumptions);