Issue #84: Disable unsafe simplification.

* When shifting disjunctive rules, we cannot simply use an existing
  (root) atom as shortcut because this could change the program's
  SCCs, which have already been computed at this point.

* Of course, instead of dropping the simplification, we could instead
  just re-compute SCCs but this would require some larger changes and
  it's not clear whether there's any benefit.

src/logic_program.cpp

@@ -1826,7 +1826,10 @@ Literal LogicProgram::getEqAtomLit(Literal lit, const BodyList& supports, Prepro
 	else if (supports.size() == 1 && supports[0]->size() < 2 && supports.back()->literal() == lit) {
 		return supports[0]->size() == 0 ? lit_true() : supports[0]->goal(0);
 	}
-	else if (p.getRootAtom(lit) != varMax) {
+	else if (p.getRootAtom(lit) != varMax && opts_.noSCC) {
+		// Use existing root atom only if scc checking is disabled.
+		// Otherwise, we would have to recheck SCCs from that atom again because
+		// adding a new edge could create a new or change an existing SCC.
 		return posLit(p.getRootAtom(lit));
 	}
 	incTrAux(1);
@@ -1835,7 +1838,8 @@ Literal LogicProgram::getEqAtomLit(Literal lit, const BodyList& supports, Prepro
 	uint32 scc   = PrgNode::noScc;
 	aux->setLiteral(lit);
 	aux->setSeen(true);
-	p.setRootAtom(aux->literal(), auxV);
+	if (p.getRootAtom(lit) == varMax)
+		p.setRootAtom(aux->literal(), auxV);
 	for (BodyList::const_iterator sIt = supports.begin(); sIt != supports.end(); ++sIt) {
 		PrgBody* b = *sIt;
 		if (b->relevant() && b->value() != value_false) {

tests/dlp_builder_test.cpp

@@ -200,6 +200,22 @@ TEST_CASE("Disjunctive logic programs", "[asp][dlp]") {
 			REQUIRE((it->user != d || it->cond == lit_false()));
 		}
 	}
+
+	SECTION("testIssue84") {
+		lpAdd(lp.start(ctx),
+			"d:-b.\n"
+			"e|f :-c, d.\n"
+			"d :-e.\n"
+			"a :-c, d.\n"
+			"{b;c }.\n");
+		REQUIRE((lp.endProgram() && ctx.endInit()));
+		const DG& graph = *ctx.sccGraph;
+
+		REQUIRE(graph.numNonHcfs() == 0);
+		CHECK(graph.numAtoms() == 4);  // bot, d, e, and either a or some new atom x
+		CHECK(graph.numBodies() == 4); // {c,d}, {b}, {e}, {a/x, not f}
+	}
+
 	SECTION("testIncremental") {
 		lp.start(ctx);
 		lp.updateProgram();

tests/facade_test.cpp

@@ -289,6 +289,20 @@ TEST_CASE("Facade", "[facade]") {
 		CHECK(out[1] == 2);
 	}
 
+	SECTION("testIssue84") {
+		config.solve.numModels = 0;
+		Clasp::Asp::LogicProgram& asp = libclasp.startAsp(config, false);
+		lpAdd(asp,
+			"d:-b.\n"
+			"t|f :-c, d.\n"
+			"d :-t.\n"
+			"a :-c, d.\n"
+			"{b;c }.\n");
+		libclasp.prepare();
+		REQUIRE(libclasp.solve().sat());
+		REQUIRE(libclasp.summary().numEnum == 5);
+	}
+
 	SECTION("testComputeBrave") {
 		config.solve.numModels = 0;
 		config.solve.enumMode = EnumOptions::enum_brave;