summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-08 18:17:24 +0100
committerSon Ho2022-02-08 18:17:24 +0100
commit83c06f5c51ac7b500e87b344f93840e9852eba91 (patch)
tree4093fdc4ddb70481845220deb00fedffca01a174
parentef59256fb354edb9d6ffee81bb3f9e82648a6d5a (diff)
Make a minor modifications to Makefile and main.ml
-rw-r--r--Makefile2
-rw-r--r--src/main.ml4
2 files changed, 3 insertions, 3 deletions
diff --git a/Makefile b/Makefile
index 22463da8..0807e092 100644
--- a/Makefile
+++ b/Makefile
@@ -14,7 +14,7 @@ build:
# Build the project and run the executable
.PHONY: build-run
build-run: build
- dune exec -- src/main.exe $(CFIM_TEST_FILE1) -dest $(DEST_DIR) > tests/trace_current.txt
+ dune exec -- src/main.exe $(CFIM_TEST_FILE1) -dest $(DEST_DIR) -test-units -test-trans-units > tests/trace_current.txt
# Build the project and run the executable, then check that the behaviour
# of the interpreter didn't change by comparing the newly generated trace
diff --git a/src/main.ml b/src/main.ml
index c30c43f2..2502ac4d 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -55,8 +55,8 @@ let () =
" Test the unit functions with the concrete interpreter" );
( "-test-trans-units",
Arg.Set test_trans_units,
- " Test the translated unit functions with the target theorem prover's \
- normalizer" );
+ " Test the translated unit functions with the target theorem\n\
+ \ prover's normalizer" );
]
in
let spec = Arg.align spec in