Fix provenance explanations for multiple constraints (#2585)

Author: jjjxia

src/ast2ram/provenance/SubproofGenerator.cpp

@@ -205,6 +205,8 @@ Own<ram::Operation> SubproofGenerator::generateReturnInstantiatedValues(const as
     for (const auto* constraint : ast::getBodyLiterals<const ast::BinaryConstraint>(clause)) {
         values.push_back(context.translateValue(*valueIndex, constraint->getLHS()));
         values.push_back(context.translateValue(*valueIndex, constraint->getRHS()));
+        values.push_back(mk<ram::UndefValue>());
+        values.push_back(mk<ram::UndefValue>());
     }
 
     // final provenance negation

tests/provenance/CMakeLists.txt

@@ -22,6 +22,7 @@ souffle_provenance_test(cprog1)
 souffle_provenance_test(eqrel_tests3 COMPILED_SPLITTED)
 souffle_provenance_test(explain_float_unsigned)
 souffle_provenance_test(high_arity)
+souffle_provenance_test(multiple_constraints)
 souffle_provenance_test(negation)
 souffle_provenance_test(path)
 souffle_provenance_test(path_explain_negation)

tests/provenance/multiple_constraints/link.csv

@@ -0,0 +1 @@
+1	2	3

tests/provenance/multiple_constraints/multiple_constraints.dl

@@ -0,0 +1,20 @@
+// Souffle - A Datalog Compiler
+// Copyright (c) 2026 The Souffle Developers. All rights reserved
+// Licensed under the Universal Permissive License v 1.0 as shown at:
+// - https://opensource.org/licenses/UPL
+// - <souffle root>/licenses/SOUFFLE-UPL.txt
+
+// This code tests provenance explanations for rules with multiple constraints.
+
+.pragma "provenance" "explain"
+
+.decl node(x: number)
+
+.decl link(x: number, y: number, z: number)
+.output link
+
+node(1).
+node(2).
+node(3).
+
+link(x, y, z) :- node(x), node(y), node(z), x < y, y < z.

tests/provenance/multiple_constraints/multiple_constraints.err

@@ -0,0 +1 @@
+explain link(1, 2, 3)

tests/provenance/multiple_constraints/multiple_constraints.in

@@ -0,0 +1,3 @@
+node(1) node(2) node(3) 1 < 2 2 < 3
+--------------------------------(R1)
+           link(1, 2, 3)