TPA: Fix bug in the analysis of transition-system chain

When backtracking from a target TS to a source TS, after the
(previously) truly reached in the source has been blocked, we compute a
new set of truly reached states in the source. Then we want to check the
edge again to the target.
However, at this point, we were trying the INITIAL states of the
target's TS. This is not correct, because we have not updated the
initial states of the TS before, we have only updated the truly safe
states, which is exactly what should be considered at this point.
We want to know if from the truly reached of source TS we can reach
something that is NOT truly safe in the target TS.

src/engine/TPA.cc

@@ -1412,7 +1412,7 @@ VerificationResult TransitionSystemNetworkManager::solve() && {
             EId nextEdge = getOutgoingEdge(current);
 //            std::cout << "Reached states in node " << current.id << ": " << logic.pp(explanation) << std::endl;
             getNode(current).trulyReached = explanation;
-            PTRef nextConditions = getInitialStates(graph.getTarget(nextEdge));
+            PTRef nextConditions = logic.mkNot(getNode(graph.getTarget(nextEdge)).trulySafe);
             auto [edgeRes, edgeExplanation] = queryEdge(nextEdge, explanation, nextConditions);
             if (reachable(edgeRes)) { // Edge propagates forward
                 auto next = graph.getTarget(nextEdge);

test/test_TPA.cc

@@ -248,6 +248,51 @@ TEST_F(TPATest, test_TPA_chain_regression) {
     solveSystem(clauses, engine, VerificationAnswer::SAFE, false);
 }
 
+TEST_F(TPATest, test_TPA_chain_regression_2) {
+    Options options;
+    options.addOption(Options::LOGIC, "QF_LIA");
+    options.addOption(Options::COMPUTE_WITNESS, "true");
+    options.addOption(Options::ENGINE, TPAEngine::SPLIT_TPA);
+    SymRef s1 = mkPredicateSymbol("inv1", {intSort()});
+    SymRef s2 = mkPredicateSymbol("inv2", {intSort()});
+    PTRef predS1Current = instantiatePredicate(s1, {x});
+    PTRef predS1Next = instantiatePredicate(s1, {xp});
+    PTRef predS2Current = instantiatePredicate(s2, {x});
+    PTRef predS2Next = instantiatePredicate(s2, {xp});
+    PTRef five = logic->mkIntConst(FastRational(5));
+    PTRef three = logic->mkIntConst(FastRational(3));
+    std::vector<ChClause> clauses{{ // x = 5 => S1(x)
+        ChcHead{UninterpretedPredicate{predS1Next}},
+        ChcBody{{logic->mkEq(xp, five)}, {}}
+    },
+        { // S1(x) and (x' = x + 1 or x' = x - 1) => S1(x')
+            ChcHead{UninterpretedPredicate{predS1Next}},
+            ChcBody{{logic->mkOr({logic->mkEq(xp, logic->mkPlus(x, one)), logic->mkEq(xp, logic->mkMinus(x, one))})},
+                {UninterpretedPredicate{predS1Current}}
+            }
+        },
+        { // S1(x) => S2(x)
+            ChcHead{UninterpretedPredicate{predS2Current}},
+            ChcBody{{logic->getTerm_true()}, {UninterpretedPredicate{predS1Current}}}
+        },
+        { // S2(x) and x > 5 and x' = x + 1 => S2(x')
+            ChcHead{UninterpretedPredicate{predS2Next}},
+            ChcBody{{logic->mkAnd(
+                logic->mkGt(x, five),
+                logic->mkEq(xp, logic->mkPlus(x, one))
+            )
+            },
+                {UninterpretedPredicate{predS2Current}}}
+        },
+        { // S2(x) and x = 3 => false
+            ChcHead{UninterpretedPredicate{logic->getTerm_false()}},
+            ChcBody{{logic->mkEq(x, three)},
+                {UninterpretedPredicate{predS2Current}}}
+        }};
+    TPAEngine engine(*logic, options);
+    solveSystem(clauses, engine, VerificationAnswer::UNSAFE);
+}
+
 TEST_F(TPATest, test_transformContractVertex_safe) {
     Options options;
     options.addOption(Options::LOGIC, "QF_LIA");