Fix regression in preprocessing of disjunctions.

* Aux atoms introduced as shortcuts for long bodies during
  (gamma) shifting must not be added to the program dependency
  graph. Otherwise, the unfounded set checker will always assign
  them to false.

src/logic_program.cpp

@@ -1248,10 +1248,9 @@ void LogicProgram::finalizeDisjunctions(Preprocessor& p, uint32 numSccs) {
 	uint32 shifted = 0;
 	stats.nonHcfs  = uint32(nonHcfs_.size());
 	Literal bot    = lit_false();
-	DlpTr tr(this, PrgEdge::Gamma);
-	RuleTransform shifter(tr);
 	Potassco::LitVec rb;
 	VarVec rh;
+	DlpTr tr(this, PrgEdge::Gamma);
 	for (uint32 id = 0, maxId = sizeVec(disj); id != maxId; ++id) {
 		PrgDisj* d = disj[id];
 		Literal dx = d->inUpper() ? d->literal() : bot;
@@ -1288,6 +1287,7 @@ void LogicProgram::finalizeDisjunctions(Preprocessor& p, uint32 numSccs) {
 		// create shortcut for supports to avoid duplications during shifting
 		Literal supportLit = dx != bot ? getEqAtomLit(dx, supports, p, sccMap) : dx;
 		// create shifted rules and split disjunctions into non-hcf components
+		RuleTransform shifter(tr);
 		for (VarVec::iterator hIt = head.begin(), hEnd = head.end(); hIt != hEnd; ++hIt) {
 			uint32 scc = getAtom(*hIt)->scc();
 			if (scc == PrgNode::noScc || (sccMap[scc] & seen_scc) != 0) {
@@ -1324,7 +1324,6 @@ void LogicProgram::finalizeDisjunctions(Preprocessor& p, uint32 numSccs) {
 						nonHcfs_.add(scc);
 					}
 					if (!options().noGamma) {
-						tr.scc = scc;
 						shifter.transform(sr, Potassco::size(sr.cond) < 4 ? RuleTransform::strategy_no_aux : RuleTransform::strategy_default);
 					}
 					else {

tests/facade_test.cpp

@@ -645,6 +645,35 @@ TEST_CASE("Facade", "[facade]") {
 	}
 };
 
+TEST_CASE("Regressions", "[facade][regression]") {
+	Clasp::ClaspFacade libclasp;
+	Clasp::ClaspConfig config;
+
+	SECTION("disjunctive shifting") {
+		config.solve.numModels = 0;
+		Clasp::Asp::LogicProgram& asp = libclasp.startAsp(config);
+		lpAdd(asp,
+			"x52 :- x2.\n"
+			"x2 :- x19.\n"
+			"x2 :- x16.\n"
+			"x6 :- x15.\n"
+			"x6 :- x14.\n"
+			"x6 :- x13.\n"
+			"x6 :- x12.\n"
+			"x19 :- x54.\n"
+			"x13 :- x60.\n"
+			"x12 :- x61.\n"
+			"x16 :- x52.\n"
+			"x12 | x13 | x14 | x15 | x16 | x19.\n"
+			"x54 :- x2.\n"
+			"x60 :- x6.\n"
+			"x61 :- x6.\n");
+		libclasp.prepare();
+		REQUIRE(libclasp.solve().sat());
+		REQUIRE(libclasp.summary().numEnum == 2);
+	}
+}
+
 TEST_CASE("Incremental solving", "[facade]") {
 	Clasp::ClaspFacade libclasp;
 	Clasp::ClaspConfig config;