Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_flattening_test / flattening_test.smt2 @ 6c3ea955

History | View | Annotate | Download (2.62 KB)

1
; flattening_test
2
(declare-var flattening_test.In1_1_1 Real)
3
(declare-var flattening_test.Out1_1_1 Real)
4
(declare-var flattening_test.ni_0._arrow._first_c Bool)
5
(declare-var flattening_test.ni_0._arrow._first_m Bool)
6
(declare-var flattening_test.ni_0._arrow._first_x Bool)
7
(declare-var flattening_test.Constant1_1_1 Real)
8
(declare-var flattening_test.Constant_1_1 Real)
9
(declare-var flattening_test.SaturationDynamic_1_1 Real)
10
(declare-var flattening_test.__flattening_test_1 Bool)
11
(declare-var flattening_test.__flattening_test_2 Bool)
12
(declare-var flattening_test.__flattening_test_3 Bool)
13
(declare-var flattening_test.i_virtual_local Real)
14
(declare-rel flattening_test_reset (Bool Bool))
15
(declare-rel flattening_test_step (Real Real Bool Bool))
16

    
17
(rule (=> 
18
  (and 
19
       
20
       (= flattening_test.ni_0._arrow._first_m true)
21
  )
22
  (flattening_test_reset flattening_test.ni_0._arrow._first_c
23
                         flattening_test.ni_0._arrow._first_m)
24
))
25

    
26
(rule (=> 
27
  (and (= flattening_test.ni_0._arrow._first_m flattening_test.ni_0._arrow._first_c)
28
       (and (= flattening_test.__flattening_test_1 (ite flattening_test.ni_0._arrow._first_m true false))
29
            (= flattening_test.ni_0._arrow._first_x false))
30
       (and (or (not (= flattening_test.__flattening_test_1 true))
31
               (= flattening_test.i_virtual_local 0.0))
32
            (or (not (= flattening_test.__flattening_test_1 false))
33
               (= flattening_test.i_virtual_local 1.0))
34
       )
35
       (= flattening_test.Constant1_1_1 1.00000000)
36
       (= flattening_test.__flattening_test_3 (< flattening_test.In1_1_1 flattening_test.Constant1_1_1))
37
       (= flattening_test.Constant_1_1 1.00000000)
38
       (= flattening_test.__flattening_test_2 (> flattening_test.In1_1_1 flattening_test.Constant_1_1))
39
       (and (or (not (= flattening_test.__flattening_test_2 true))
40
               (= flattening_test.SaturationDynamic_1_1 flattening_test.Constant_1_1))
41
            (or (not (= flattening_test.__flattening_test_2 false))
42
               (and (or (not (= flattening_test.__flattening_test_3 true))
43
                       (= flattening_test.SaturationDynamic_1_1 flattening_test.Constant1_1_1))
44
                    (or (not (= flattening_test.__flattening_test_3 false))
45
                       (= flattening_test.SaturationDynamic_1_1 flattening_test.In1_1_1))
46
               ))
47
       )
48
       (= flattening_test.Out1_1_1 flattening_test.SaturationDynamic_1_1)
49
       )
50
  (flattening_test_step flattening_test.In1_1_1
51
                        flattening_test.Out1_1_1
52
                        flattening_test.ni_0._arrow._first_c
53
                        flattening_test.ni_0._arrow._first_x)
54
))
55