[CN] Discrepency in queries sent to CVC5 vs Z3

[yav]

To reproduce:

timeout 30 cn verify <path-to>/cn-tutorial/src/examples/queue_pop.c --solver-type=z3 --solver-logging=queue_pop_z3_31161e9e7
timeout 30 cn verify <path-to>/cn-tutorial/src/examples/queue_pop.c --solver-type=cvc5 --solver-logging=queue_pop_cvc5_31161e9e7
diff --color=always -u queue_pop_z3_31161e9e7/z3_send_0.smt queue_pop_cvc5_31161e9e7/cvc5_send_0.smt | head -n 50

--- queue_pop_z3_31161e9e7/z3_send_0.smt        2024-08-22 08:59:15
+++ queue_pop_cvc5_31161e9e7/cvc5_send_0.smt    2024-08-22 09:09:34
@@ -1274,1036 +1274,3970 @@
 (assert
  (and
   (not
-   (not
-    (= (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708))
-     (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)))))))
-(check-sat)
-(get-model)
-(pop 1)
-(push 1)

[yav]

I looked into this, and I don't think it's a bug. What appears to be happening is:

• CN's type-checker makes decisions based on the model (e.g., see model_has_prop)
• The different solver produce different models. So because of that we sometimes take slightly different paths to the goal. @cp526 does this sound right?

[cp526]

That sounds plausible.

[yav]

Great, I'll close this then, thanks!