Test failure with latest Z3 on MacOSX

[damiendr]

Hello,

I'm using MacOSX 10.6 and have a version of Z3 4.1.2 compiled from the source code available at: http://z3.codeplex.com/

I have cloned the ScalaZ3 git repo (oct. 10) and followed the instructions in the README file. I had to place the lib and include files in a folder called "4.0" and not "4.1.2" in order to get through the following steps:

$ sbt update $ sbt package

Then I get some errors when I run the tests:

$ DYLD_LIBRARY_PATH=z3/x64/4.0/lib/ sbt test [info] == load-lib == [info] [info] == copy-test-resources == [info] == copy-test-resources == [info] [info] == test-start == [info] == test-start == [info] [info] == IntArith == [info] IntArith: [info] - Comfusy-like [info] == IntArith == [info] [info] == TheoryExtension == [info] TheoryExtension: Problem 0, should be solved by simplifying only (no model). Problem 1. [info] - Theory extension [info] == TheoryExtension == [info] [info] == NQueens == [info] NQueens: Total number of models: 92 [info] - NQueens [info] == NQueens == [info] [info] == Core == [info] Core: [info] - Core [info] == Core == [info] [info] == ADTs == [info] ADTs: [info] - ADTs [info] == ADTs == [info] [info] == ForComprehension == [info] ForComprehension: [info] - ForComprehension [info] == ForComprehension == [info] [info] == Calendar == [info] Calendar: [info] - Calendar [info] == Calendar == [info] [info] == QuickPA == [info] QuickPA: Sat? -> sat Unsat? -> unsat WARNING: invalid function application, sort mismatch on argument at position 1 Invalid memory access of location 0x0 rip=0x11294a526

Segmentation fault

[psuter]

Hi, it's hard to tell what is going on here. I just tried ScalaZ3 with the latest version of Z3 (from Git) and I do not observe the error in the same way: QuickPA fails, but does not crash.

This particular testcase relies on the theory plugin mechanism of Z3. I'll have to take a look to see if something changed in this particular part of the interface. Note that Leo also pointed out that it was now becoming obsolete.

I would imagine that other parts of Z3 work fine for you?

[damiendr]

Well, it seems that most other things are working fine. I removed QuickPA from the test suite and the other tests pass, except for Arrays. Is that expected?

[info] == Arrays ==
[info] Arrays:
model is
arr!0 -> as-array[k!4]
x!2 -> 42
arr!1 -> as-array[k!5]
ft!3 -> 1
k!4 -> {
  6 -> 42
  else -> 42
}
k!5 -> {
  2 -> 0
  6 -> 42
  else -> 42
}

When evaluated, array1 is: Some((Map(6 -> 42),42))
When evaluated, array2 is: Some((Map(2 -> 0, 6 -> 42),42))
[info] - Arrays *** FAILED ***
[info]   None did not equal Some(42) (Arrays.scala:68)

[damiendr]

Right, the comments in the code say these are expected to fail. I guess I can safely use the rest of ScalaZ3! Thanks for looking into it.

[psuter]

Indeed. Both problems should still be fixed (or in the QuickPA case maybe removed from the repo), so I'm opening separate issues for them.