Could not satisfy all constraints for regression test

[jfecher]

Aim

Tried to prove and verify the regression test

Expected Behavior

The test should produce a valid proof

Bug

The test fails to prove and verify, outputtting the message: Could not satisfy all constraints

To Reproduce

Installation Method

None

Nargo Version

No response

Additional Context

No response

Would you like to submit a PR for this Issue?

No

Support Needs

No response

[jfecher]

After #1815, this also affects sha2_byte and sha2_blocks

Edit: All the sha tests are fixed now.

[jfecher]

Observation: changing main's parameters from witnesses to constants by adding:

    let x = [0x3f, 0x1c, 0xb8, 0x99, 0xab];
    let z = 3;

to the beginning of main makes the test pass.

[kevaundray]

Minimal example:

fn main(input: u8, length: Field) -> pub Field
{
    if input != 1 {}
    else
    {
     let cond = (0 as u64) < (length as u64) - 1;
     if cond{}
    }

    input as Field
}

// Prover.toml
input = 0x3f
length = 3

Note, input does not equal 1, so the then branch should be getting triggered, however we are getting constrained failed on the else branch. Changing input != 1 to input == 1 will produce a passing program

[kevaundray]

Error for reference ^

[kevaundray]

This error seems to stem from the fact that we are not multiplying the predicate by the expression which constrains the quotient directive, we therefore account for all cases except for when q ==0 and r ==0