Panic exception when proof-logging

[IgnaceBleukx]

Hi,

I'm using Pumpkin to generate a proof of an unsatisfiable jobshop model. I got a some error triggered in the solver:

thread '<unnamed>' panicked at pumpkin-solver/src/engine/constraint_satisfaction_solver.rs:1567:17:
assertion failed: self.assignments_propositional.is_literal_assigned_true(premise)

The code below should generate a minimal-ish example (it's still quite elaborate...)

from pumpkin_py import Model
from pumpkin_py import constraints
import numpy as np

model = Model()

add  = model.add_constraint # shortcut
impl = model.add_implication # shortcut

s = np.array([[model.new_integer_variable(0,50,name=f"s_[{i},{j}]") for j in range(2)] for i in range(3)])
e = np.array([[model.new_integer_variable(0, 50,name=f"e_[{i},{j}]") for j in range(2)] for i in range(3)])

add(constraints.Cumulative(list(s[:,0]), [7, 1, 9], [1, 1, 1], 1))
add(constraints.BinaryEquals(s[0, 0].offset(7), e[0, 0]))
add(constraints.BinaryEquals(s[1, 0].offset(1), e[1, 0]))
add(constraints.BinaryEquals(s[2, 0].offset(9), e[2, 0]))

add(constraints.Cumulative(list(s[:,1]), [7, 5, 8], [1, 1, 1], 1))
add(constraints.BinaryEquals(s[0, 1].offset(7), e[0, 1]))
add(constraints.BinaryEquals(s[1, 1].offset(5), e[1, 1]))
add(constraints.BinaryEquals(s[2, 1].offset(8), e[2, 1]))

# precedence constraints
add(constraints.BinaryLessThanEqual(e[0,0], s[0,1]))
add(constraints.BinaryLessThanEqual(e[1, 0], s[1, 1]))
add(constraints.BinaryLessThanEqual(e[2, 0], s[2, 1]))

# encode maximum
max_var = model.new_integer_variable(0,50,name="max_var")
add(constraints.LessThanOrEquals([max_var], 24))

add(constraints.BinaryLessThanEqual(e[0, 0], max_var))
add(constraints.BinaryLessThanEqual(e[0, 1], max_var))
add(constraints.BinaryLessThanEqual(e[1, 0], max_var))
add(constraints.BinaryLessThanEqual(e[1, 1], max_var))
add(constraints.BinaryLessThanEqual(e[2, 0], max_var))
add(constraints.BinaryLessThanEqual(e[2, 1], max_var))

model.satisfy(proof="proof")

When disabling the proof-logging it works fine.

Currently running on the main branch (commit c1dd091)

[maartenflippo]

I think I fixed this now, try running on cd7a35b6edbf.