Unexpected SyGuS error: A non-linear fact was asserted to arithmetic in a linear logic

[daniel-larraz]

Describe the bug cvc5 fails with error A non-linear fact was asserted to arithmetic in a linear logic on this SyGuS problem:

(set-logic LIA)

(synth-fun f ( (x Int) ) Int

  (( y_int Int ) ( y_const_int Int ) ( y_bool Bool ) )

  (( y_int Int (
     y_const_int
     (- y_int )
     (+ y_int y_int)
     (- y_int y_int)
     (* y_const_int y_int)
     (* y_int y_const_int)
     (div y_int y_const_int)
     (mod y_int y_const_int)
     (abs y_int)
     (ite y_bool y_int y_int))
   )

   ( y_const_int Int (( Constant Int )))

   ( y_bool Bool (
     (= y_int y_int)
     (> y_int y_int)
     (>= y_int y_int)
     (< y_int y_int)
     (<= y_int y_int))
   ))
)

(declare-var x Int)

(constraint (>= (f x) x))

(check-synth)

Notice the grammar for f follows the reference grammar for integer-typed terms in LIA without free variables.

cvc5 version/commit: ea4d18e Operating system: Linux

[ajreynol]

This is caused by evaluation unfolding lemmas, --sygus-eval-unfold=none avoids the issue.

We should refactor how constants in grammars are handled to avoid this kind of issue.

[daniel-larraz]

Thank you for suggesting the workaround!