Adjusted SC_tac, adjusted change_compspecs warning message, store_tac

PrincetonUniversity / VST

Verified Software Toolchain

https://vst.cs.princeton.edu

Other

424 stars 91 forks source link

Adjusted SC_tac, adjusted change_compspecs warning message, store_tac #739

Closed andrew-appel closed 8 months ago

andrew-appel commented 8 months ago

Adjusted SC_tac so it is more careful and doesn't break things; made the new warning message in change_compspecs user-disablable; fixed a unification blowup in store_tac.

andrew-appel commented 8 months ago

the commit message that refers to load_tac should have said store_tac.

andrew-appel commented 8 months ago

@lennartberinger can you test this against your examples on which the try simple apply eq_refl in SC_tac was causing problems?