Entered Unreachable code in proof-logging

[IgnaceBleukx]

Hi,

I'm trying to find a proof-log of an unsatisfiable Sudoku model.
When solving without proof-logging, the solver concludes correctly that the model is UNSAT.
However, when enabling proof-logging, I get the following error:

thread '<unnamed>' panicked at pumpkin-solver/src/engine/constraint_satisfaction_solver.rs:1320:21:
internal error: entered unreachable code
stack backtrace:
0: rust_begin_unwind
         at /rustc/e71f9a9a98b0faf423844bf0ba7438f29dc27d58/library/std/src/panicking.rs:665:5
1: core::panicking::panic_fmt
         at /rustc/e71f9a9a98b0faf423844bf0ba7438f29dc27d58/library/core/src/panicking.rs:76:14
2: core::panicking::panic
         at /rustc/e71f9a9a98b0faf423844bf0ba7438f29dc27d58/library/core/src/panicking.rs:148:5
3: pumpkin_solver::engine::constraint_satisfaction_solver::ConstraintSatisfactionSolver::log_root_propagation_to_proof
         at /home/ignace/git/Pumpkin/pumpkin-solver/src/engine/constraint_satisfaction_solver.rs:1320:21
4: pumpkin_solver::engine::constraint_satisfaction_solver::ConstraintSatisfactionSolver::propagate
         at /home/ignace/git/Pumpkin/pumpkin-solver/src/engine/constraint_satisfaction_solver.rs:1180:17
5: pumpkin_solver::engine::constraint_satisfaction_solver::ConstraintSatisfactionSolver::solve_internal
         at /home/ignace/git/Pumpkin/pumpkin-solver/src/engine/constraint_satisfaction_solver.rs:770:13
6: pumpkin_solver::engine::constraint_satisfaction_solver::ConstraintSatisfactionSolver::solve_under_assumptions
         at /home/ignace/git/Pumpkin/pumpkin-solver/src/engine/constraint_satisfaction_solver.rs:471:22
7: pumpkin_solver::engine::constraint_satisfaction_solver::ConstraintSatisfactionSolver::solve
         at /home/ignace/git/Pumpkin/pumpkin-solver/src/engine/constraint_satisfaction_solver.rs:455:9
8: pumpkin_solver::api::solver::Solver::satisfy
         at /home/ignace/git/Pumpkin/pumpkin-solver/src/api/solver.rs:311:15
9: pumpkin_py::model::Model::satisfy
         at /home/ignace/git/Pumpkin/pumpkin-py/src/model.rs:163:15
10: pumpkin_py::model::Model::__pymethod_satisfy__
         at /home/ignace/git/Pumpkin/pumpkin-py/src/model.rs:41:1

Full model (in Python) below - I'm currently running on the develop branch (commit 94e76035)

import pumpkin_py as pm
from pumpkin_py import constraints
import numpy as np

givens = np.array([[0, 0, 0, 0, 7, 0, 2, 0, 6],
                    [0, 0, 0, 0, 0, 0, 4, 0, 1],
                    [0, 0, 2, 0, 8, 0, 0, 0, 0],
                    [0, 0, 6, 0, 0, 5, 0, 0, 8],
                    [7, 0, 0, 2, 0, 0, 5, 9, 0],
                    [0, 0, 9, 0, 4, 8, 0, 0, 0],
                    [0, 5, 0, 0, 9, 6, 8, 0, 2],
                    [0, 2, 0, 8, 0, 0, 0, 0, 0],
                    [0, 0, 0, 0, 2, 0, 0, 6, 0]])


model = pm.Model()

cells = np.array([[model.new_integer_variable(1,9, f"cell{[i,j]}") for i in range(9)] for j in range(9)])

# Row constraints
for row in cells:
    model.add_constraint(constraints.AllDifferent(row.tolist()))

# Column constraints
for col in cells.T:
    model.add_constraint(constraints.AllDifferent(col.tolist()))

# Block constraints
for i in range(0,9,3):
    for j in range(0,9,3):
        block = cells[i:i+3, j:j+3]
        model.add_constraint(constraints.AllDifferent(list(block.flat)))

# set given values
for i in range(9):
    for j in range(9):
        if givens[i,j] != 0:
            model.add_constraint(constraints.Equals([cells[i,j]], givens[i,j]))


print("Solving without prooflog")
print(model.satisfy())


print("Solving with prooflog")
print(model.satisfy(proof="proof"))

[maartenflippo]

We also run into the problem that the nogood propagator introduces an inference. This inference has no tag. This shows up in the sudoku experiment