Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / kind_fmcad08 / simulation / Gas.smt2 @ 2d37a1e1

History | View | Annotate | Download (1.8 KB)

1
(set-logic AUFNIRA)
2
(declare-fun leak () Bool)
3
(declare-fun P1 () Bool)
4
(declare-fun fresh_4 () Bool)
5
(declare-fun fresh_6 () Int)
6
(declare-fun fresh_9 () Bool)
7
(declare-fun xxx_init () Bool)
8
(declare-fun fresh_2 () Int)
9
(declare-fun fresh_1 () Bool)
10
(declare-fun fresh_10 () Bool)
11
(declare-fun fresh_12 () Bool)
12
(declare-fun fresh_8 () Int)
13
(declare-fun fresh_11 () Int)
14
(declare-fun fresh_13 () Int)
15
(declare-fun memi (Int Int Int) Bool)
16
(declare-fun memu (Int Int) Bool)
17
(declare-fun memi (Bool Bool Bool) Bool)
18
(declare-fun memu (Bool Bool) Bool)
19
(assert (let ((top_0_Age_6_P1 (not P1))) (let ((top_0_RaisingEdge_2_res (ite xxx_init false (and (not fresh_9) P1)))) (let ((top_0_Age_3_P1 (not leak))) (let ((top_0_Age_3_Count (ite xxx_init 0 (ite fresh_1 (+ fresh_2 1) 0)))) (let ((top_0_Age_0_Count (ite xxx_init 0 (ite fresh_10 (+ fresh_6 1) 0)))) (let ((top_0_Sofar_1_X (<= top_0_Age_0_Count 10))) (let ((top_0_Sofar_1_Sofar (ite xxx_init top_0_Sofar_1_X (and top_0_Sofar_1_X fresh_4)))) (let ((top_0_env (and top_0_Sofar_1_Sofar (or (not top_0_RaisingEdge_2_res) (<= 300 top_0_Age_3_Count))))) (let ((top_0_Age_6_Count (ite xxx_init 0 (ite fresh_12 (+ fresh_8 1) 0)))) (let ((top_0_Dursince_5_Count (ite xxx_init 0 (ite fresh_9 0 (ite fresh_10 (+ fresh_11 1) fresh_11))))) (let ((top_0_Age_4_Count (ite xxx_init 0 (ite fresh_12 (+ fresh_13 1) 0)))) (let ((top_0_OK (or (not top_0_env) (or (<= top_0_Age_4_Count 600) (<= (* 2 top_0_Dursince_5_Count) top_0_Age_6_Count))))) (and (memu  fresh_4 top_0_Sofar_1_Sofar) (memu  fresh_6 top_0_Age_0_Count) (memu  fresh_9 P1) (memi  xxx_init true false) (memu  fresh_2 top_0_Age_3_Count) (memu  fresh_1 top_0_Age_3_P1) (memu  fresh_10 leak) (memu  fresh_12 top_0_Age_6_P1) (memu  fresh_8 top_0_Age_6_Count) (memu  fresh_11 top_0_Dursince_5_Count) (memu  fresh_13 top_0_Age_4_Count)))))))))))))))