From fbc8f62a180e92b1bd0cd37c0a9bb0fae9c4f791 Mon Sep 17 00:00:00 2001
From: Viktor Malik <viktor.malik@gmail.com>
Date: Fri, 26 Jun 2020 13:03:49 +0200
Subject: [PATCH 1/2] Makefile: fix path from 2LS to CBMC

---
 Makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index 5e14420..ebef430 100644
--- a/Makefile
+++ b/Makefile
@@ -46,14 +46,14 @@ cbmc.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC
 	cd $(basename $@) && rm cbmc cbmc-binary goto-cc LICENSE README
 	rmdir $(basename $@)
 
-2ls.zip: 2ls.inc tool-wrapper.inc $(2LS)/LICENSE $(2LS)/src/2ls/2ls $(2LS)/cbmc/src/goto-cc/goto-cc sv-comp-readme.sh
+2ls.zip: 2ls.inc tool-wrapper.inc $(2LS)/LICENSE $(2LS)/src/2ls/2ls $(2LS)/lib/cbmc/src/goto-cc/goto-cc sv-comp-readme.sh
 	mkdir -p $(basename $@)
 	$(MAKE) 2ls-wrapper
 	mv 2ls-wrapper $(basename $@)/2ls
 	./sv-comp-readme.sh $(basename $@) > $(basename $@)/README
 	cp -L $(2LS)/LICENSE $(basename $@)/
 	cp -L $(2LS)/src/2ls/2ls $(basename $@)/2ls-binary
-	cp -L $(2LS)/cbmc/src/goto-cc/goto-cc $(basename $@)/
+	cp -L $(2LS)/lib/cbmc/src/goto-cc/goto-cc $(basename $@)/
 	chmod a+rX $(basename $@)/*
 	zip -r $@ $(basename $@)
 	cd $(basename $@) && rm 2ls 2ls-binary goto-cc LICENSE README

From 425df58ca30833c49d21afcf3da562989c513b7b Mon Sep 17 00:00:00 2001
From: Viktor Malik <viktor.malik@gmail.com>
Date: Fri, 26 Jun 2020 13:04:28 +0200
Subject: [PATCH 2/2] 2LS: new default CLI options

---
 2ls.inc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/2ls.inc b/2ls.inc
index 26c5863..b58b53f 100644
--- a/2ls.inc
+++ b/2ls.inc
@@ -60,7 +60,7 @@ run()
       fi
     fi
   else
-    PROPERTY="$PROPERTY --heap-values-refine --sympath --k-induction --competition-mode"
+    PROPERTY="$PROPERTY --heap --values-refine --k-induction --competition-mode"
 
     # run the tool
     $TOOL_BINARY --graphml-witness $LOG.witness --object-bits $OBJ_BITS $PROPERTY \