From b6676f6dc3b1471317cce8e04e9cb7203168f75c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 11 Nov 2022 16:05:56 +0100
Subject: Make minor modifications to the tests and regenerate the .fst files

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

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 2c324a41..3f04ff09 100644
--- a/Makefile
+++ b/Makefile
@@ -86,7 +86,7 @@ clean:
 tests: trans-no_nested_borrows trans-paper \
 	trans-hashmap trans-hashmap_main \
 	trans-external trans-constants \
-	trans-polonius-betree_polonius trans-polonius-betree_main \
+	trans-polonius-polonius_list trans-polonius-betree_main \
 	test-trans-polonius-betree_main
 
 # Verify the F* files generated by the translation
@@ -106,7 +106,7 @@ CHARON_CMD = cd $(CHARON_TEST_DIR) && NOT_ALL_TESTS=1 $(MAKE) test-$*
 endif
 
 # The command to run Aeneas on the proper llbc file
-AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest ../tests/$(SUBDIR) $(OPTIONS)
+AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(SUBDIR) $(OPTIONS)
 
 
 # Add specific options to some tests
@@ -120,8 +120,8 @@ trans-hashmap: SUBDIR:=hashmap
 trans-hashmap_main: OPTIONS += -template-clauses
 trans-hashmap_main: SUBDIR:=hashmap_on_disk
 
-trans-polonius-betree_polonius: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
-trans-polonius-betree_polonius: SUBDIR:=misc
+trans-polonius-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
+trans-polonius-polonius_list: SUBDIR:=misc
 
 trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
 trans-constants: SUBDIR:=misc
-- 
cgit v1.2.3