Bug #55
assertions generation in Horn clauses (smt2 file)
0%
Description
with the file attached
Using Unstable branch I get following errors using these steps:
lustrec -horn tcm_with_properties_PP.lus
Successfully generates smt2 file
z3 tcm_with_properties_PP.smt2
(error "line 4438 column 56: unknown constant tcm_with_properties_PP_TCM_Heading.__tcm_with_properties_PP_TCM_Heading_10")
(error "line 4685 column 59: unknown constant tcm_with_properties_PP_TCM_Longitudinal.__tcm_with_properties_PP_TCM_Longitudinal_6")
(error "line 6242 column 102: unknown constant tcm_with_properties_PP_TCM_AutoThrottle_AutoThrottle_Subsystem_Guide_100_Env.__tcm_with_properties_PP_TCM_AutoThrottle_AutoThrottle_Subsystem_Guide_100_Env_8")
(error "line 6765 column 66: unknown constant tcm_with_properties_PP_TCM_Heading_Guide_260.__tcm_with_properties_PP_TCM_Heading_Guide_260_14")
(error "line 6955 column 98: unknown constant tcm_with_properties_PP_TCM_AutoThrottle_AutoThrottle_Subsystem_Guide_290.__tcm_with_properties_PP_TCM_AutoThrottle_AutoThrottle_Subsystem_Guide_290_5")
(error "line 7967 column 98: unknown constant tcm_with_properties_PP_TCM_AutoThrottle_AutoThrottle_Subsystem_Guide_100.__tcm_with_properties_PP_TCM_AutoThrottle_AutoThrottle_Subsystem_Guide_100_8")
(error "line 8255 column 80: unknown constant tcm_with_properties_PP_TCM_Longitudinal_Guide_200_Simple.__tcm_with_properties_PP_TCM_Longitudinal_Guide_200_Simple_7")
(error "line 8978 column 71: unknown constant tcm_with_properties_PP_TCM_Heading_Guide_250.__tcm_with_properties_PP_TCM_Heading_Guide_250_3")
(error "line 9753 column 77: unknown constant tcm_with_properties_PP_TCM_Longitudinal_Guide_200_Env.__tcm_with_properties_PP_TCM_Longitudinal_Guide_200_Env_11")
(error "line 10171 column 71: unknown constant tcm_with_properties_PP_TCM_Heading_Guide_240.__tcm_with_properties_PP_TCM_Heading_Guide_240_4")
History
#1 Updated by Pierre-Loïc Garoche over 2 years ago
- Status changed from New to Closed
#2 Updated by Anonymous 6 months ago
Speaking of apps and scanning barcodes, you can scan your barcode with the Legit Check App and see if you have a fake or real Yeezy Boost 350 V2 pair, and we will teach you how to scan your barcode in a few seconds.
[[https://www.buyyzys.com/tag/fake-yeezy-website/]]