Passing a list of assumptions in solver.checkAssumptions?

[greninja]

Hey, I want to pass a list of assumption literals in solver.checkAssumptions (in order to get the Unsat Core). I have Z3 version 4.4.1 on my machine and I have tried with both scalaz3_2.10-3.0.jar and scalaz3-unix-64b-2.1.1.jar.

Supposedly I have 4 propositional literals - a,b,c,d and I want to pass all of them to solver.checkAssumptions. Surprisingly, this works :

solver.checkAssumptions(a,b,c,d)

but, assuming alist = List(a,b,c,d) :

solver.checkAssumptions(alist) throws the following error :

scala> solver.checkAssumptions(alist) 
<console>:22: error: type mismatch;
 found   : List[z3.scala.Z3AST] 
 required: z3.scala.Z3AST  
              solver.checkAssumptions(alist)

I checked the code for checkAssumptions in Z3Solver and it says :

def checkAssumptions(assumptions: Z3AST*) : Option[Boolean] = {

which implies I should be able to pass a list/Seq/array of assumptions right? Could anyone help?

[greninja]

I think I got it! Stupid mistake!

[romac]

For anyone else who stumbles on this issue:

def checkAssumptions(assumptions: Z3AST*) : Option[Boolean]

says that checkAssumptions takes a variable number of arguments of type Z3AST which will all be bundled into the assumptions parameter. The assumptions variable will thus have type Seq[Z3AST].

If one wants to splice a list of arguments to a varargs method, one must use the following syntax:

val alist = List(a,b,c,d)
solver.checkAssumptions(alist: _*)