search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
332 stars 62 forks source link

Some tests fail #53

Closed yurivict closed 5 years ago

yurivict commented 5 years ago 
 268/1800 Test  #268: modelgen ....................................   Passed    0.08 sec
          Start  269: modelgen1
 269/1800 Test  #269: modelgen1 ...................................Child aborted***Exception:   0.13 sec
          Start  270: modelgen10
 270/1800 Test  #270: modelgen10 ..................................Child aborted***Exception:   0.09 sec
          Start  271: modelgen11
 271/1800 Test  #271: modelgen11 ..................................Child aborted***Exception:   0.09 sec
          Start  272: modelgen12
 272/1800 Test  #272: modelgen12 ..................................Child aborted***Exception:   0.09 sec
          Start  273: modelgen13
 273/1800 Test  #273: modelgen13 ..................................Child aborted***Exception:   0.09 sec
          Start  274: modelgen14
 274/1800 Test  #274: modelgen14 ..................................Child aborted***Exception:   0.09 sec

Example of the individual failure log:

$ ctest --verbose -R modelgen20
UpdateCTestConfiguration  from :/usr/ports/math/boolector/work/.build/DartConfiguration.tcl
UpdateCTestConfiguration  from :/usr/ports/math/boolector/work/.build/DartConfiguration.tcl
Test project /usr/ports/math/boolector/work/.build
Constructing a list of tests
Done constructing a list of tests
Updating test list for fixtures
Added 0 tests to meet fixture requirements
Checking test dependency graph...
Checking test dependency graph end
test 281
    Start 281: modelgen20

281: Test command: /usr/ports/math/boolector/work/.build/bin/test "-q" "-e" "modelgen20"
281: Test timeout computed to be: 10000000
281:   File "/usr/ports/math/boolector/work/boolector-3.0.0-239-g0b4b8540/contrib/btorcheckmodel.py", line 11
281:     print "Usage: ./btorcheckmodel <btor-file> <btor-output-model-file> <boolector-binary>"
281:                                                                                           ^
281: SyntaxError: Missing parentheses in call to 'print'. Did you mean print("Usage: ./btorcheckmodel <btor-file> <btor-output-model-file> <boolector-binary>")?
281: Assertion failed: (ret_val == 0), function modelgen_test, file /usr/ports/math/boolector/work/boolector-3.0.0-239-g0b4b8540/test/testmodelgen.c, line 92.
1/1 Test #281: modelgen20 .......................Child aborted***Exception:   0.12 sec

0% tests passed, 1 tests failed out of 1

Total Test time (real) =   0.22 sec

The following tests FAILED:
    281 - modelgen20 (Child aborted)
Errors while running CTest
mpreiner commented 5 years ago

Seems like the Python script is not Python 3 compatible. I'll have a closer look.