Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_flattening_4_test / flattening_4_test.smt2 @ 6c3ea955

History | View | Annotate | Download (1.55 KB)

1
; flattening_4_test
2
(declare-var flattening_4_test.In1_1_1 Real)
3
(declare-var flattening_4_test.Out1_1_1 Real)
4
(declare-var flattening_4_test.ni_0._arrow._first_c Bool)
5
(declare-var flattening_4_test.ni_0._arrow._first_m Bool)
6
(declare-var flattening_4_test.ni_0._arrow._first_x Bool)
7
(declare-var flattening_4_test.__flattening_4_test_1 Bool)
8
(declare-var flattening_4_test.i_virtual_local Real)
9
(declare-rel flattening_4_test_reset (Bool Bool))
10
(declare-rel flattening_4_test_step (Real Real Bool Bool))
11

    
12
(rule (=> 
13
  (and 
14
       
15
       (= flattening_4_test.ni_0._arrow._first_m true)
16
  )
17
  (flattening_4_test_reset flattening_4_test.ni_0._arrow._first_c
18
                           flattening_4_test.ni_0._arrow._first_m)
19
))
20

    
21
(rule (=> 
22
  (and (= flattening_4_test.ni_0._arrow._first_m flattening_4_test.ni_0._arrow._first_c)
23
       (and (= flattening_4_test.__flattening_4_test_1 (ite flattening_4_test.ni_0._arrow._first_m true false))
24
            (= flattening_4_test.ni_0._arrow._first_x false))
25
       (and (or (not (= flattening_4_test.__flattening_4_test_1 true))
26
               (= flattening_4_test.i_virtual_local 0.0))
27
            (or (not (= flattening_4_test.__flattening_4_test_1 false))
28
               (= flattening_4_test.i_virtual_local 1.0))
29
       )
30
       (= flattening_4_test.Out1_1_1 flattening_4_test.In1_1_1)
31
       )
32
  (flattening_4_test_step flattening_4_test.In1_1_1
33
                          flattening_4_test.Out1_1_1
34
                          flattening_4_test.ni_0._arrow._first_c
35
                          flattening_4_test.ni_0._arrow._first_x)
36
))
37