Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CI: "`logicString' is a bad argument" test failures #1223

Closed
RyanGlScott opened this issue Jun 25, 2021 · 3 comments
Closed

CI: "`logicString' is a bad argument" test failures #1223

RyanGlScott opened this issue Jun 25, 2021 · 3 comments
Assignees
Labels
CI Continuous integration prover Issues related to :sat and :prove

Comments

@RyanGlScott
Copy link
Contributor

RyanGlScott commented Jun 25, 2021

The poly.icry test case (among others) fails on the test (test-lib, regression, ubuntu-latest, false) job. See here and here for examples of where it happens. It looks like this:

      poly.icry: [Failed]
1a2,7
> Warning: solver interaction failed with w4-cvc4
>     Received parsed and understood but unexpected response from solver:
>   AckSuccessSExp (SApp [SAtom "error",SString "Parse Error: Illegal argument detected\n\n  (set-logic ALL_SUPPORTED)\n             ^\n\nvoid cvc5::LogicInfo::setLogicString(std::__cxx11::string)\n\n  `logicString' is a bad argument\nLogicInfo::setLogicString(): junk (",SAtom "LL_SUPPORTED",SString ") at end of logic string: ALL_SUPPORTED"])
> in response to command for sat result:
>   (check-sat)
> 
13,17c19,25
< 	Q.E.D.
< :prove polyAddEval
< 	Q.E.D.
< :prove polyMulEval
< 	Q.E.D.
---
> 	
> What4 exception:
> Received parsed and understood but unexpected response from solver:
>   AckSuccessSExp (SApp [SAtom "error",SString "Parse Error: Illegal argument detected\n\n  (set-logic ALL_SUPPORTED)\n             ^\n\nvoid cvc5::LogicInfo::setLogicString(std::__cxx11::string)\n\n  `logicString' is a bad argument\nLogicInfo::setLogicString(): junk (",SAtom "LL_SUPPORTED",SString ") at end of logic string: ALL_SUPPORTED"])
> in response to command for sat result:
>   (check-sat)
> 
@RyanGlScott RyanGlScott added the CI Continuous integration label Jun 25, 2021
@robdockins
Copy link
Contributor

Is is sporadic? I think it's reliably occurring, but only on specific platforms.

@RyanGlScott RyanGlScott changed the title CI: Sporadic "`logicString' is a bad argument" test failures CI: "`logicString' is a bad argument" test failures Jun 30, 2021
@RyanGlScott
Copy link
Contributor Author

Hm. I could have sworn that restarting the CI managed to fix this, but perhaps I've misremembered. Given that practically all recent CI jobs have failed with this error, I'll remove the word "Sporadic" from the issue title.

@kquick kquick assigned kquick and unassigned lisanna-dettwyler Jul 2, 2021
@robdockins robdockins added the prover Issues related to :sat and :prove label Jul 14, 2021
@robdockins
Copy link
Contributor

This seems like it is a CI configuration issue, which has (at least temporarily) been resolved. Feel free to reopen if this starts happening again.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CI Continuous integration prover Issues related to :sat and :prove
Projects
None yet
Development

No branches or pull requests

4 participants