search

CJex / hol-light

HOL Light is an interactive theorem prover / proof checker. Automatically exported from code.google.com/p/hol-light
Other
1 stars 0 forks source link

Examples/prog.ml: VC_TAC has trouble with with single-variable programs #26

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
What steps will reproduce the problem?

Execute these commands:
# needs "Examples/prog.ml";;
# install_parser ("correct",parse_program_assertion);;
# g `correct
     T
       var x;
       x := 1
       end
     x > 0`;;
# e VC_TAC;;

What is the expected output? What do you see instead?

VC_TAC should generate verification conditions `1 > 0`, but it leaves the goal 
unmodified.

What version of the product are you using? On what operating system?

HOL Light from SVN, revision 200; ocaml 4.01.0, Linux

Please provide any additional information below.

VC_TAC works as expected if I introduce a dummy variable:

# g `correct T var x, dummy; x := 1 end x > 0`;;

Original issue reported on code.google.com by piotr.tr...@gmail.com on 20 Oct 2014 at 9:50