Integer*real symbolic multiplication gives cryptic error message `(unknown)`

[natebragg]

The following program:

#lang rosette

(define-symbolic* x integer?)
(define-symbolic* y real?)

(synthesize
  #:forall (list x y)
  #:guarantee
  (assert (<= 0 (* (* x y) x))))

Gives the following cryptic error:

application: not a procedure;
 expected a procedure that can be applied to arguments
  given: (unknown)
  context...:
   ~/.racket/8.15/pkgs/rosette/rosette/query/eval.rkt:19:0: eval-rec
   .../match/compiler.rkt:559:40: f29
   ~/.racket/8.15/pkgs/rosette/rosette/query/eval.rkt:19:0: eval-rec
   .../match/compiler.rkt:559:40: f29
   ~/.racket/8.15/pkgs/rosette/rosette/query/eval.rkt:19:0: eval-rec
   .../match/compiler.rkt:559:40: f29
   ~/.racket/8.15/pkgs/rosette/rosette/query/eval.rkt:19:0: eval-rec
   .../match/compiler.rkt:559:40: f21
   ~/.racket/8.15/pkgs/rosette/rosette/query/eval.rkt:19:0: eval-rec
   ~/.racket/8.15/pkgs/rosette/rosette/query/core.rkt:151:0: cegis
   ~/.racket/8.15/pkgs/rosette/rosette/query/core.rkt:129:6

Obviously it should just fail to synthesize since that property can't hold forall x,y.

If I tweak the program to include the hole p, and ignore y in the guarantee:

#lang rosette

(define-symbolic* x integer?)
(define-symbolic* y real?)
(define-symbolic* p real?)

(synthesize
  #:forall (list x y)
  #:guarantee
  (assert (<= 0 (* (* x p) x))))

It succeeds with the result (model [p$2 0.0]).

What is this (unknown)? Is this program impossible but with a confusing error message, or is this just a straightforward bug? In the meantime, is there an equivalent program I can write that guarantees an equivalent property? For context, this is a simplified version of a different program I wanted to write, with p and y restricted to fewer values.

[emina]

The original problem is undecidable, because x has integer? type so this becomes non-linear arithmetic over integers. So, the solver returns unknown (rather than sat or unsat) because it's unable to solve it.

This version (non-linear arithmetic over reals) is decidable and returns unsat:

#lang rosette

(define-symbolic* x real?)
(define-symbolic* y real?)

(synthesize
  #:forall (list x y)
  #:guarantee
  (assert (<= 0 (* (* x y) x))))

[natebragg]

Ah, in that case I would argue that this error message is confusing, since I'm not sure what I should do next to try to resolve it. Would it be possible to replace it with one that makes the issue clear? I'm sure that something to the effect of your reply would be sufficiently informative. Thank you!