build: Replace ls_nonrec_entail_ls_{07 => 05}.sb.smt2 and add kore smoke test

Author: nishantjr

prover/build

@@ -131,8 +131,10 @@ secondary_tests('qf_shidlia_entl_unsat_tests', 't/test-lists/qf_shidlia_entl.uns
 secondary_tests('qf_shlid_entl_unsat_tests',   't/test-lists/qf_shlid_entl.unsat')
 secondary_tests('shid_entl_unsat_tests',       't/test-lists/shid_entl.unsat')
 
+def test_path(name, type):
+    return ".build/t/%s.prover-%s-krun" % (name, type)
 def sl_comp_test_path(name):
-    return ".build/t/SL-COMP18/bench/qf_shid_entl/%s.prover-smt-krun" % (name)
+    return test_path("SL-COMP18/bench/qf_shid_entl/%s" % name, 'smt')
 
 proj.alias('smoke-tests', list(map( sl_comp_test_path, [ 
            "02.tst.smt2"                         , # RList trans 
@@ -145,9 +147,12 @@ proj.alias('smoke-tests', list(map( sl_comp_test_path, [
            "skl2-vc03.smt2"                      , # needs framing but not match-pto 
            "odd-lseg3_slk-5.smt2"                , # needs framing and match-pto 
            "nll-vc01.smt2"                       , # needs large number of unfolding but no kt
-           "ls_nonrec_entail_ls_07.sb.smt2"      , # 6 variable transitivity: ls_nonrec(x,x1) * ... * ls_nonrec(x4,x5) -> ls(x,x5)  - needs large number of kts and unfolding
+           "ls_nonrec_entail_ls_05.sb.smt2"      , # 4 variable transitivity: ls_nonrec(x,x1) * ... * ls_nonrec(x4,x5) -> ls(x,x5)  - needs large number of kts and unfolding
            "ls_lsrev_concat_entail_ls_1.sb.smt2" , # need unfolding within implication context
-          ])))
+          ])) +
+          [ test_path('t/listSegmentLeft-implies-listSegmentRight.kore', 'kore')
+          ]
+          )
 
 # Unit Tests
 # ----------