Nonterminating SyGuS problem

[BillHallahan]

When run on this SyGuS problem:

(set-logic ALL)
(define-fun safe-mod ((x Int) (y Int)) Int (mod x (+ 1 (abs y))))

(synth-fun f 
    ((r Int)) Bool 
    ((B Bool) )
    (
        (B Bool (true)) 
    )
)

(synth-fun g 
    ((x0 Int) (r Int)) Bool 
    ((B Bool) (I Int) (IConst Int)) 
    (
        (B Bool ((<= I I) ))
        (I Int ((Variable Int) (+ I I) (* I I) (safe-mod I IConst)))
        (IConst Int ((Constant Int)))
    )
)

; (constraint (f 2))

(constraint (g 2 8))
(constraint (g (- 2) (- 8)))
(constraint (not (g 0 (- 1))))

(check-synth)

CVC4 does not terminate (I left it running for 10 minutes.)

CVC4 finds a solution in under a second if the constraint on f is uncommented, or if (safe-mod I IConst) is removed from the grammar for g .

Command line arguments: cvc4 test.sl --lang=sygus2 CVC4 version/commit: This is CVC4 version 1.8-prerelease [git master 5489ef01] compiled with GCC version 4.2.1 Compatible Apple LLVM 11.0.0 (clang-1100.0.33.17) on Feb 20 2020 21:29:19 Operating system: MacOS

[ajreynol]

This behavior is due to nonlinear arithmetic, see discussion on CVC4/CVC4#3800.

[ajreynol]

This benchmark solves quickly in latest master (https://github.com/cvc5/cvc5/commit/231eaa4afb7f65d14e75170ef74c75a6d1def7bc).