Project

General

Profile

Bug #55

assertions generation in Horn clauses (smt2 file)

Added by Hamza Bourbouh over 3 years ago. Updated 1 day ago.

Status:
Closed
Priority:
High
Category:
Bug
Start date:
05/24/2017
Due date:
% Done:

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")

tcm_with_properties_PP.lus (104 KB) Hamza Bourbouh, 05/24/2017 11:25 PM

History

#1 Updated by Pierre-Loïc Garoche about 2 years ago

  • Status changed from New to Closed
Comment

Solved in current unstable version 1.5-827

#2 Updated by Anonymous 1 day ago

Comment

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/]]

Also available in: Atom PDF