CN: Fix CI

[dc-mak]

For some reason this test is causing a CI failure related to SMT issues that is not reproducible locally: #663

[dc-mak]

E.g like this:

[./cn/record1.c]...
./cn/record1.c:13:18: warning: Treating exponentiation 'power(2'i32
  , 31'i32 /* 0x1f */)' as uninterpreted.
/*@ requires x < power(2i32, 31i32) - 1i32; 
                 ~~~~~^~~~~~~~~~~~~ 
./cn/record1.c:14:18: warning: Treating exponentiation 'power(2'i32
  , 31'i32 /* 0x1f */)' as uninterpreted.
    requires y < power(2i32, 31i32) - 1i32; @*/
                 ~~~~~^~~~~~~~~~~~~ 
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
    Called from Cn__Solver.provable in file "backend/cn/lib/solver.ml", line 1409, characters 4-68
    Called from Cn__ResourceInference.General.parametric_ftyp_args_request_step in file "backend/cn/lib/resourceInference.ml", line 142, characters 16-26
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.sandbox in file "backend/cn/lib/typing.ml", line 86, characters 10-13
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.run_from_pause in file "backend/cn/lib/typing.ml", line 68, characters 50-55
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 169, characters 6-443
    Re-raised at Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 188, characters 4-69
    Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
    Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44
FAIL (Unexpected return code: 125)

It started here: https://github.com/rems-project/cerberus/actions/runs/11468005495/job/31949217625 but that doesn't seem related. Could be related to the Z3 used by the VM used by the CI.

[podhrmic]

This can be caused by the different installation - in the CI, you are pinning various packages, but not calling make in the process. While for the local install, I am assuming you are calling the makefiles as mentioned in the documentation - is that correct?

[podhrmic]

[This MR] is an attempt to at least unify the docker and CI builds, but it is still not clear which way of building/installing Cerberus/CN is the right one.

[dc-mak]

Pinning the packages should be the same as calling the Makefile (see the Makefile and opam files). Also, the link to the PR in your comment is broken.