Fix SideCondition normalization error (#2239)

* Pattern.simplify: Avoid SideCondition normalization problems

* Add test/issue-2221

Author: ttuegel

kore/src/Kore/Step/Simplification/Pattern.hs

@@ -11,6 +11,7 @@ module Kore.Step.Simplification.Pattern
 import Prelude.Kore
 
 
+import qualified Kore.Internal.Condition as Condition
 import qualified Kore.Internal.Conditional as Conditional
 import Kore.Internal.OrPattern
     ( OrPattern
@@ -75,8 +76,19 @@ simplify sideCondition pattern' =
         let (term, simplifiedCondition) =
                 Conditional.splitTerm withSimplifiedCondition
             term' = substitute (toMap $ substitution simplifiedCondition) term
+            simplifiedCondition' =
+                -- Combine the predicate and the substitution. The substitution
+                -- has already been applied to the term being simplified. This
+                -- is only to make SideCondition.andCondition happy, below,
+                -- because there might be substitution variables in
+                -- sideCondition. That's allowed because we are only going to
+                -- send the side condition to the solver, but we should probably
+                -- fix SideCondition.andCondition instead.
+                simplifiedCondition
+                & Condition.toPredicate
+                & Condition.fromPredicate
             termSideCondition =
-                sideCondition `SideCondition.andCondition` simplifiedCondition
+                sideCondition `SideCondition.andCondition` simplifiedCondition'
         simplifiedTerm <- simplifyConditionalTerm termSideCondition term'
         let simplifiedPattern =
                 Conditional.andCondition simplifiedTerm simplifiedCondition

test/issue-2221/Makefile

@@ -0,0 +1 @@
+include $(CURDIR)/../include.mk

test/issue-2221/spec.kore

@@ -0,0 +1,17 @@
+[]
+module INVALID-SIZE
+
+// imports
+import LIST-SIZER []
+
+
+// claims
+// claim `<generatedTop>`(`<k>`(inj{MyList,KItem}(_0)),_DotVar0,`<size>`(#token("0","Int")))=>`<generatedTop>`(`<k>`(.K),_DotVar0,`<size>`(#token("0","Int"))) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(9), contentStartLine(4), org.kframework.attributes.Location(Location(4,9,5,25)), org.kframework.attributes.Source(Source(/home/stephen/work/k-experiments/list-sizer/././specs/invalid-size.spec)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
+  claim{} \implies{SortGeneratedTopCell{}} (
+      \and{SortGeneratedTopCell{}} (
+      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortMyList{}, SortKItem{}}(Var'Unds'0:SortMyList{}),dotk{}())),Var'Unds'DotVar0:SortGeneratedCounterCell{},Lbl'-LT-'size'-GT-'{}(\dv{SortInt{}}("0")))), weakAlwaysFinally{SortGeneratedTopCell{}} (
+      \and{SortGeneratedTopCell{}} (
+      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(dotk{}()),Var'Unds'DotVar0:SortGeneratedCounterCell{},Lbl'-LT-'size'-GT-'{}(\dv{SortInt{}}("0"))))))
+  [org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/stephen/work/k-experiments/list-sizer/././specs/invalid-size.spec)"), org'Stop'kframework'Stop'definition'Stop'Production{}(), contentStartLine{}(), contentStartColumn{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(4,9,5,25)")]
+
+endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1,1,6,9)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/stephen/work/k-experiments/list-sizer/././specs/invalid-size.spec)")]

test/issue-2221/test-issue-2221.sh

@@ -0,0 +1,16 @@
+#!/bin/sh
+exec kore-exec \
+    vdefinition.kore \
+    --module LIST-SIZER \
+    --smt-timeout 40 \
+    --smt z3 \
+    --strategy all \
+    --log-level \
+    warning \
+    --enable-log-timestamps \
+    --prove spec.kore \
+    --spec-module INVALID-SIZE \
+    --graph-search breadth-first \
+     \
+     \
+    "$@"

test/issue-2221/test-issue-2221.sh.out.golden

@@ -0,0 +1,36 @@
+/* Created: Kore.Internal.OrPattern.toTermLike */
+/* Spa */
+\and{SortGeneratedTopCell{}}(
+    /* Fl Fn D Sfa */
+    Lbl'-LT-'generatedTop'-GT-'{}(
+        /* Fl Fn D Sfa Cl */ Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()),
+        /* Fl Fn D Sfa */
+        Lbl'-LT-'generatedCounter'-GT-'{}(
+            /* Fl Fn D Sfa */ Var'Unds'DotVar1:SortInt{}
+        ),
+        /* Fl Fn D Sfa Cl */
+        Lbl'-LT-'size'-GT-'{}(
+            /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("1")
+        )
+    ),
+    /* Created: Kore.Internal.Predicate.makeAndPredicate */
+    /* Spa */
+    \and{SortGeneratedTopCell{}}(
+        /* Spa */
+        \equals{SortMyList{}, SortGeneratedTopCell{}}(
+            /* Fl Fn D Sfa */ Var'Unds'0:SortMyList{},
+            /* Fl Fn D Sfa */
+            Lbl'UndsUndsUnds'LIST-SIZER-SYNTAX'Unds'MyList'Unds'Int'Unds'MyList{}(
+                /* Fl Fn D Sfa */ Var'Unds'E:SortInt{},
+                /* Fl Fn D Sfa Cl */
+                Lbl'Stop'MyList'Unds'LIST-SIZER-SYNTAX'Unds'MyList{}()
+            )
+        ),
+        /* Spa */
+        \equals{SortMyList{}, SortGeneratedTopCell{}}(
+            /* Fl Fn D Sfa */ VarL:SortMyList{},
+            /* Fl Fn D Sfa Cl */
+            Lbl'Stop'MyList'Unds'LIST-SIZER-SYNTAX'Unds'MyList{}()
+        )
+    )
+)