[CN] Use Z3 >= 4.8.13 and re-add record1.c test to CI

[dc-mak]

tests/cn/record1.c:

/*@
function ({i32 x, i32 y}) increment(i32 x, i32 y) {
    {x: x + 1i32, y: y + 1i32}
}

function ({i32 x, i32 y}) decrement(i32 x, i32 y) {
    {x: x - 1i32, y: y - 1i32}
}

@*/

signed int incr_one(signed int x, signed int y, int flag)
/*@ requires x < power(2i32, 31i32) - 1i32;
    requires y < power(2i32, 31i32) - 1i32; @*/
/*@ ensures let pair_record = increment(x, y);
    return == ((flag == 1i32) ? pair_record.x : pair_record.y); @*/
{
    return (flag == 1) ? x + 1 : y + 1;
}

signed int decr_one(signed int x, signed int y, int flag)
/*@ requires x >= 0i32;
    requires y >= 0i32; @*/
/*@ ensures let pair_record = decrement(x, y);
    return == ((flag == 1i32) ? pair_record.x : pair_record.y); @*/
{
    return (flag == 1) ? x - 1 : y - 1;
}



int main(void)
/*@ trusted; @*/
{
    signed int x = 4;
    signed int y = 2;
    signed int r1 = incr_one(x, y, 1);
    signed int r2 = incr_one(x, y, 0);

    signed int r3 = decr_one(x, y, 1);
    signed int r4 = decr_one(x, y, 0);
    return 0;
}

[dc-mak]

Related: #645

[dc-mak]

Ok, so commit 9a1868e removed the Z3 dependency from CN & Cerberus. The lower-bound for this was 4.8.14, however the version of the default Ubuntu 22.04 Jammy is 4.8.12.

This difference in version seems to be either exposing a bug in Z3, or in CN.

[0.343582] failed to ack:
(assert
 (and
  (not
   (= (bvadd x_783 #x00000001)
    (ite (= flag_781 #x00000001)
     (cn_get_0_of_2
      (cn_tuple_2 (bvadd x_783 #x00000001) (bvadd y_782 #x00000001)))
     (cn_get_1_of_2
      (cn_tuple_2 (bvadd x_783 #x00000001) (bvadd y_782 #x00000001))))))))
[0.343738]
|~~~~~~ Start Solver Dump ~~~~~~~|
# Symbols
| flag |-> flag_781
# Basetypes
+---------------------------------
# Symbols
| allocs |-> allocs_1
| &ARG0 |-> &ARG0_825
| &ARG1 |-> &ARG1_826
| &ARG2 |-> &ARG2_827
# Basetypes
| alloc_id |-> default_uf_2
+---------------------------------
# Symbols
| y |-> y_782
| x |-> x_783
# Basetypes
| i32 |-> exp_uf_1
+---------------------------------
# Symbols
# Basetypes
+---------------------------------
# Symbols
# Basetypes
+---------------------------------
|~~~~~~ End Solver Dump ~~~~~~~~~|
cn: internal error, uncaught exception:
    UnexpectedSolverResponse((error
      "line 727 column 67: unknown constant cn_tuple_2 ((_ BitVec 32) (_ BitVec 32)) \
     \ndeclared: (declare-fun cn_tuple_2\
     \n             ((_ BitVec 64) (_ BitVec 64))\
     \n             (cn_tuple_2 (_ BitVec 64) (_ BitVec 64))) "))
    Raised at Cn__Solver.debug_ack_command in file "backend/cn/lib/solver.ml", line 164, characters 4-42

[dc-mak]

Ok with --solver-logging it looks like the file is fine and Z3 is the problem. Z3 version 4.8.13 and CVC5 are both happy, but the older Z3 version is not. The solution would be to update to a more recent Z3 version in the CI.