Skip to content

Conversation

@andreiburdusa
Copy link
Contributor


Fixes #2010

Reviewer checklist
  • Test coverage: stack test --coverage
  • Public API documentation: stack haddock

@andreiburdusa andreiburdusa marked this pull request as ready for review July 28, 2020 11:55
@andreiburdusa
Copy link
Contributor Author

I used a small .k file to test this and the productivity was down to 87%

@ttuegel ttuegel self-requested a review July 28, 2020 14:03
Comment on lines 173 to 180
isSymbolic =
Foldable.any isSomeConfigVariableName substitutionVariables
|| isNothing
( getConstructorLike
. Attribute.constructorLikeAttribute
. extractAttributes
$ term configuration
)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we only need to check that the configuration is not constructor-like:

Suggested change
isSymbolic =
Foldable.any isSomeConfigVariableName substitutionVariables
|| isNothing
( getConstructorLike
. Attribute.constructorLikeAttribute
. extractAttributes
$ term configuration
)
isSymbolic = (not . isConstructorLike) (term configuration)

x |-> _0
</state>
</T>
#Not ( #Exists I . {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This test is not right. I think we should remove it.

@andreiburdusa andreiburdusa requested a review from ttuegel July 30, 2020 07:39
@ttuegel
Copy link
Contributor

ttuegel commented Jul 30, 2020

One more thing: can you please add the example from the issue as an integration test?

@rv-jenkins rv-jenkins merged commit 7860c96 into runtimeverification:master Jul 31, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Unable to narrow on results of uninterpretted functions

3 participants