diff --git a/Makefile b/Makefile index e4a64a3..098ecec 100644 --- a/Makefile +++ b/Makefile @@ -1,3 +1,5 @@ +SHELL := /bin/bash + EXE_NAME := symwhile TEST_NAME := mike_example @@ -19,6 +21,6 @@ sanity_check: which z3 test: native - ./$(EXE_NAME).native res/$(TEST_NAME).while + ./$(EXE_NAME).native --semantics symbolic <(echo "input(x); input(y); assert not (y = 0); result := x / y") .PHONY: all clean native byte sanity diff --git a/res/log_iterated_div.while b/res/log_iterated_div.while deleted file mode 100644 index 52d19ad..0000000 --- a/res/log_iterated_div.while +++ /dev/null @@ -1,10 +0,0 @@ -input(num); -input(base); - -result := 0; - -while not (num = 1) do - assert not (base = 0); - num := num / base; - result := result + 1 -done diff --git a/src/symwhile.ml b/src/symwhile.ml index ef20db4..4847c31 100644 --- a/src/symwhile.ml +++ b/src/symwhile.ml @@ -27,7 +27,7 @@ let main () = | "symbolic" -> sem := Symbolic | _ -> raise (Arg.Bad "--semantics (concrete|symbolic)")), "Choose semantics with which to run `while` stmt. (default = \"concrete\")"); - ] (function s -> input := s) "usage: sym-while (|--)"; + ] (function s -> input := s) "usage: sym-while "; let chan = open_in !input in let lexbuf = Lexing.from_channel chan in