Search code examples
z3

Z3 v4.1 does not accept negative integers as input

I have installed Z3 version 4.1 and I attempt to use it programmatically in a java application. My application is communicating with the Z3 via ProcessBuilder. The version of Z3 is verified as 4.1 by using the /version command line argument.

However, Z3 does not accept negative constants as part of expressions. When I attempt to provide a negative integers I get the following message:

(error "line 4 column 31: unknown constant -1")

This is the input I provide to Z3:

(push)
(declare-fun y () Int )
(define-fun x () Int y )
(assert (and (<= y 1000) (>= y -1) ) )
(assert (= x 42) )
(check-sat)
(pop)

I am using the following arguments to instantiate the Z3:

Z3 /smt2 /in /t:2

Any help is appreciated. Thank you in advance.

Solution

  • Try (- 1). See bottom of page 38 in http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf