qsphan / az3 Goto Github PK

Hi all,

I'm trying to get started with aZ3 with a simple example. Here the content of the smtlib2 input file:

(set-option :produce-models true)
(set-logic QF_LIA)
(declare-fun constraint1 () Bool)
(declare-fun constraint2 () Bool)
(declare-fun x () Int)
(assert (= constraint1 (> x 0)))
(assert (= constraint2 (< x 5)))
(assert (and constraint1 constraint2))
(check-allsat (constraint1 constraint2))
(allsat-relevant x)

I use the BlockingClause method to get the model count for the variable x. I expected that the solver results with the model count 4 (x=1, 2, 3, 4). But I get the following output:

BlockingClause Solver
( 
 (  (x 1 )  (constraint1 true )  (constraint2 true )  )

) 

There are 1 models
Elapsed time is 14 ms

Am I doing something wrong, or does the solver only handles the propagated boolean expressions?

Thanks,
Yannic

It says:

Running java -jar aZ3 without parameters can give you a list of options.

It should say:

Running java -jar aZ3.jar aZ3 without parameters can give you a list of options.