MR: keep quantified const assumptions

Author: tanyongkiam

keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/btactics/DLBySubst.scala

@@ -338,7 +338,7 @@ private object DLBySubst {
           else sequent.ante.map(fml =>
             ghosts.foldLeft(fml)({ case (f, ((what, repl), _)) => SubstitutionHelper.replaceFree(f)(what, repl) })).
             flatMap(FormulaTools.conjuncts).
-            filter(StaticSemantics.symbols(_).intersect(aBVs.toSet).isEmpty).toList
+            filter(StaticSemantics.freeVars(_).intersect(aBVs.toSet).isEmpty).toList
         (constConjuncts, isGame) match {
           case (Nil, _) | (_, true) => (oldifiedC, skip, implyR(1))
           case (consts, false) => (And(consts.reduceRight(And), oldifiedC),

keymaerax-webui/src/test/scala/btactics/DLTests.scala

@@ -350,6 +350,11 @@ class DLTests extends TacticTestBase {
     result.subgoals shouldBe "A>1&x>5 ==> [x:=A;]x>1".asSequent :: "A>1, x>1 ==> [y:=A*x;]y>1".asSequent :: Nil
   }
 
+  it should "preserve a quantified const fact" in withMathematica { _ =>
+    val result = proveBy("\\forall x (x^2+2>=A)&A>1&x>5 -> [x:=A;][y:=A*x;]y>1".asFormula, implyR(1) & generalize("x>1".asFormula)(1))
+    result.subgoals shouldBe "\\forall x (x^2+2>=A)&A>1&x>5 ==> [x:=A;]x>1".asSequent :: "\\forall x (x^2+2>=A)&A>1, x>1 ==> [y:=A*x;]y>1".asSequent :: Nil
+  }
+
   it should "preserve function facts" in withMathematica { _ =>
     val result = proveBy("A()>1&x>5 -> [x:=A();][y:=A()*x;]y>1".asFormula, implyR(1) & generalize("x>1".asFormula)(1))
     result.subgoals shouldBe "A()>1&x>5 ==> [x:=A();]x>1".asSequent :: "A()>1, x>1 ==> [y:=A()*x;]y>1".asSequent :: Nil