diff --git a/kore/src/Kore/Log/ErrorRewritesInstantiation.hs b/kore/src/Kore/Log/ErrorRewritesInstantiation.hs index b7acad1b97..5ceeb57a6d 100644 --- a/kore/src/Kore/Log/ErrorRewritesInstantiation.hs +++ b/kore/src/Kore/Log/ErrorRewritesInstantiation.hs @@ -15,8 +15,6 @@ import Control.Exception ( Exception (..) , throw ) -import qualified Data.Foldable as Foldable -import qualified Data.Map.Strict as Map import Data.Set ( Set ) @@ -40,7 +38,9 @@ import Kore.Internal.Conditional import Kore.Internal.Pattern ( Pattern ) -import qualified Kore.Internal.Substitution as Substitution +import Kore.Internal.TermLike + ( isConstructorLike + ) import Kore.Internal.Variable ( SomeVariableName ) @@ -158,8 +158,6 @@ checkSubstitutionCoverage configuration solution substitutionCoverageError = SubstitutionCoverageError { solution, missingVariables } - Conditional { substitution } = solution - substitutionVariables = Map.keysSet (Substitution.toMap substitution) missingVariables = wouldNarrowWith solution isCoveringSubstitution = Set.null missingVariables - isSymbolic = Foldable.any isSomeConfigVariableName substitutionVariables + isSymbolic = (not . isConstructorLike) (term configuration) diff --git a/test/imp/disjunction-in-simplification-spec.k b/test/imp/disjunction-in-simplification-spec.k deleted file mode 100644 index d84fdec848..0000000000 --- a/test/imp/disjunction-in-simplification-spec.k +++ /dev/null @@ -1,32 +0,0 @@ -/* -*/ - -module VERIFICATION - imports IMP - - syntax Id ::= "a" [token] - syntax Id ::= "b" [token] - syntax Id ::= "x" [token] - syntax AExp ::= choice (AExp, AExp) [strict] - rule choice(A:Int, B:Int) => A #Or B [simplification, anywhere] -endmodule - - -module DISJUNCTION-IN-SIMPLIFICATION-SPEC - imports VERIFICATION - imports IMP - - rule - - x = choice(a, b) ; - => .K - - - a |-> A:Int - b |-> B:Int - x |-> (_ => ?X:Int) - - ensures - ?X ==Int A orBool ?X ==Int B - -endmodule diff --git a/test/imp/disjunction-in-simplification-spec.k.out.golden b/test/imp/disjunction-in-simplification-spec.k.out.golden deleted file mode 100644 index 999d53f9be..0000000000 --- a/test/imp/disjunction-in-simplification-spec.k.out.golden +++ /dev/null @@ -1,10 +0,0 @@ - - - x = choice ( a , b ); ~> . - - - a |-> A:Int - b |-> B:Int - x |-> _0 - - diff --git a/test/issue-2010/1.test b/test/issue-2010/1.test new file mode 100644 index 0000000000..300ddfaeb1 --- /dev/null +++ b/test/issue-2010/1.test @@ -0,0 +1 @@ +f() \ No newline at end of file diff --git a/test/issue-2010/1.test.out.golden b/test/issue-2010/1.test.out.golden new file mode 100644 index 0000000000..b01636f936 --- /dev/null +++ b/test/issue-2010/1.test.out.golden @@ -0,0 +1,3 @@ + + I:Int ~> . + diff --git a/test/issue-2010/Makefile b/test/issue-2010/Makefile new file mode 100644 index 0000000000..caa7b2e4b4 --- /dev/null +++ b/test/issue-2010/Makefile @@ -0,0 +1 @@ +include $(CURDIR)/../include.mk diff --git a/test/issue-2010/test.k b/test/issue-2010/test.k new file mode 100644 index 0000000000..3253e357a1 --- /dev/null +++ b/test/issue-2010/test.k @@ -0,0 +1,13 @@ +module TEST + imports BOOL + imports INT + + syntax MaybeInt ::= "Some" Int + | "None" + syntax MaybeInt ::= f() [function, functional, no-evaluators] + + configuration f() + + rule None => true ... + rule Some I => I ... +endmodule \ No newline at end of file