13 lines
597 B
Text
13 lines
597 B
Text
|
(assert (>= |CELL_actual_input_0_0_0| (/ 4278419646001971 4503599627370496)))
|
||
|
|
(assert (< |CELL_actual_input_0_0_0| (/ 1 1)))
|
||
|
|
(assert (>= |CELL_actual_input_0_0_1| (/ 4278419646001971 4503599627370496)))
|
||
|
|
(assert (< |CELL_actual_input_0_0_1| (/ 1 1)))
|
||
|
|
(assert (>= |CELL_actual_input_0_0_2| (/ 4278419646001971 4503599627370496)))
|
||
|
|
(assert (< |CELL_actual_input_0_0_2| (/ 1 1)))
|
||
|
|
(assert (>= |CELL_actual_output_0_0_0| (/ 0 1)))
|
||
|
|
(check-sat)
|
||
|
|
(get-value (|CELL_actual_input_0_0_0|))
|
||
|
|
(get-value (|CELL_actual_input_0_0_1|))
|
||
|
|
(get-value (|CELL_actual_input_0_0_2|))
|
||
|
|
(get-value (|CELL_actual_output_0_0_0|))
|