search

epfl-lara / ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver
Apache License 2.0
122 stars 34 forks source link

z3 for osx #1

Closed eaubin closed 12 years ago

eaubin commented 12 years ago

Since z3 had an osx release last week I took a crack at getting it to compile on my mac. A few of the tests fail though:

[info] SatSolver: [info] - Sat solver * FAILED * [info] java.util.NoSuchElementException: None.get [info] at scala.None$.get(Option.scala:274) [info] at scala.None$.get(Option.scala:272) [info] at SatSolver$$anonfun$1$$anonfun$DPLL$1$4.apply(SatSolver.scala:53) [info] at SatSolver$$anonfun$1$$anonfun$DPLL$1$4.apply(SatSolver.scala:53) [info] at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:194) [info] at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:194) [info] at scala.collection.mutable.HashMap$$anonfun$foreach$1.apply(HashMap.scala:93) [info] at scala.collection.mutable.HashMap$$anonfun$foreach$1.apply(HashMap.scala:93) [info] at scala.collection.Iterator$class.foreach(Iterator.scala:660) [info] at scala.collection.mutable.HashTable$$anon$1.foreach(HashTable.scala:157) [info] ...

[info] - Arrays * FAILED * [info] Some(1) did not equal Some(42) (Arrays.scala:64)

[info] - Literals * FAILED * [info] 3 did not equal 4 (Literals.scala:60)

psuter commented 12 years ago

Sorry, I didn't comment on the tests: that's unrelated to the platform, we need to clarify what's wrong with them anyway (i.e. is it Z3, the bindings or the test itself).