search

GaloisInc / what4

Symbolic formula representation and solver interaction library
155 stars 13 forks source link

what4-1.5.1 testsuite failures in stackage lts 22 #262

Closed juhp closed 6 months ago

juhp commented 6 months ago 
       Test suite failure for package what4-1.5.1                                                                                   
           abduct:  exited with: ExitFailure 1                                                                                      
           invariant-synthesis:  exited with: ExitFailure 1                                                                         
           template_tests:  exited with: ExitFailure 1
           Tests                                                                                                                    
             testing SAT query for abduction:      FAIL                                                                             
               Exception: user error (Could not find: cvc5)                                                                         
               Use -p '/testing SAT query for abduction/' to rerun this test only.                                                  
             getting 3 abducts using cvc5 offline: FAIL                                                                             
               Exception: cvc5: createProcess: posix_spawnp: does not exist (No such file or directory)                             
               Use -p '/getting 3 abducts using cvc5 offline/' to rerun this test only.
             getting 3 abducts using cvc5 online:  FAIL
               Exception: user error (Could not find: cvc5)
               Use -p '/getting 3 abducts using cvc5 online/' to rerun this test only.
           Tests
             int cvc5 test: FAIL
               Exception: user error (Could not find: cvc5)
               Use -p '/int cvc5 test/' to rerun this test only.
             int z3 test:   OK (0.09s)
             bv cvc5 test:  FAIL
               Exception: user error (Could not find: cvc5)
               Use -p '/bv cvc5 test/' to rerun this test only.
juhp commented 6 months ago

Ah maybe cvc5 should be installed?

RyanGlScott commented 6 months ago

Yes, that's correct.

juhp commented 6 months ago

Okay I will park such a change for nightly, probably not worth it for lts22.

Hope I caught all the failures: there is a lot of stack output