evaluate spec rules with requires constraints when initializing

daejunpark · daejunpark · commit 3d3f8e1938e0 · 2018-05-07T02:04:42.000-05:00
diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/InitializeRewriter.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/InitializeRewriter.java
@@ -322,8 +322,8 @@ public ProcessProofRules invoke(GlobalContext rewritingContext, long initCounter
                         .map(r -> converter.convert(Optional.<Module>empty(), r))
                         .map(r -> new org.kframework.backend.java.kil.Rule(
                                 r.label(),
-                                r.leftHandSide().evaluate(termContext),
-                                r.rightHandSide().evaluate(termContext),
+                                evaluate(r.leftHandSide(), r.getRequires(), termContext),
+                                evaluate(r.rightHandSide(), r.getRequires(), termContext),
                                 r.requires(),
                                 r.ensures(),
                                 r.freshConstants(),
@@ -334,6 +334,13 @@ public ProcessProofRules invoke(GlobalContext rewritingContext, long initCounter
                         .collect(Collectors.toList());
                 return this;
             }
+
+            private Term evaluate(Term term, ConjunctiveFormula constraint, TermContext context) {
+                context.setTopConstraint(constraint);
+                Term newTerm = term.evaluate(context);
+                context.setTopConstraint(null);
+                return newTerm;
+            }
         }
     }
 
