agacek

(declare-const actionName String)
(declare-const actionNamespace String)
(declare-const |aws:securetransport| Bool)
(declare-const |aws:securetransport_exists| Bool)
(declare-const principalProviderTermBit0 Bool)
(declare-const principalProviderTermBit1 Bool)
(declare-const principal_account String)
(declare-const principal_partition String)
(declare-const principal_prefix String)
(declare-const principal_region String)

agacek

(declare-fun x8828 () Bool)
(declare-fun x87843 () Bool)
(declare-fun x44512 () Bool)
(declare-fun x48062 () Bool)
(declare-fun x19674 () Bool)
(declare-fun x75985 () Bool)
(declare-fun x62050 () Bool)
(declare-fun x89209 () Bool)
(declare-fun x21309 () Bool)
(declare-fun x67904 () Bool)

agacek

(set-logic QF_UFLIRA)

(declare-fun i1 () Int)
(declare-fun i2 () Int)

(declare-fun b1 () Bool)
(declare-fun b2 () Bool)
(declare-fun b3 () Bool)

(declare-fun r1 () Real)

agacek

(define-state-type state ((|%init| Bool) (|signal| Real) (|errorA| Real) (|errorB| Real) (|errorC| Real) (|output| Real) (|difference| Real) (|sensedA| Real) (|sensedB| Real) (|sensedC| Real) (|equalizedA| Real) (|equalizedB| Real) (|equalizedC| Real) (|equalizationA| Real) (|equalizationB| Real) (|equalizationC| Real) (|pre_output| Real) (|centering| Real) (|pre_equalizedA| Real) (|pre_equalizedB| Real) (|pre_equalizedC| Real) (|lemmaA| Bool) (|lemmaB| Bool) (|lemmaC| Bool) (|ok1| Bool) (|ok2| Bool) (|ok3| Bool) (|ok4| Bool) (|ok5| Bool) (|abs~0.a| Real) (|abs~0.out| Real) (|abs~1.a| Real) (|abs~1.out| Real) (|abs~2.a| Real) (|abs~2.out| Real) (|middleValue~0.a| Real) (|middleValue~0.b| Real) (|middleValue~0.c| Real) (|middleValue~0.out| Real) (|equalization~0.centering_value| Real) (|equalization~0.equalized_value| Real) (|equalization~0.output_value| Real) (|equalization~0.equalization_value| Real) (|equalization~0.sum1| Real) (|equalization~0.sum2| Real) (|equalization~0.sat1| Real) (|equalization~0.sat2|

agacek

node initial(a : bool) returns (holds : bool);
let
   holds = a -> true ;
tel ;

node before_always(p : bool; a : bool) returns (holds : bool);
var
   state : subrange [-1,3] of int;
   pre_state : subrange [-1,3] of int;

agacek

(define-fun T ((%init Bool) ($signal$0 Real) ($errorA$0 Real) ($errorB$0 Real) ($errorC$0 Real) ($difference$0 Real) ($sensedA$0 Real) ($sensedB$0 Real) ($sensedC$0 Real) ($equalizedA$0 Real) ($equalizedB$0 Real) ($equalizedC$0 Real) ($pre_output$0 Real) ($centering$0 Real) ($pre_equalizedA$0 Real) ($pre_equalizedB$0 Real) ($pre_equalizedC$0 Real) ($lemmaA$0 Bool) ($lemmaB$0 Bool) ($lemmaC$0 Bool) ($ok1$0 Bool) ($ok2$0 Bool) ($ok3$0 Bool) ($ok4$0 Bool) ($ok5$0 Bool) ($abs~0.out$0 Real) ($abs~1.out$0 Real) ($abs~2.out$0 Real) ($middleValue~0.out$0 Real) ($equalization~0.equalization_value$0 Real) ($equalization~0.sum1$0 Real) ($equalization~0.sum2$0 Real) ($equalization~1.equalization_value$0 Real) ($equalization~1.sum1$0 Real) ($equalization~1.sum2$0 Real) ($equalization~2.equalization_value$0 Real) ($equalization~2.sum1$0 Real) ($equalization~2.sum2$0 Real) ($middleValue~1.out$0 Real) ($abs~3.a$0 Real) ($abs~3.out$0 Real) ($abs~4.a$0 Real) ($abs~4.out$0 Real) ($abs~5.a$0 Real) ($abs~5.out$0 Real) ($abs~6.out

agacek

(set-option :produce-interpolants true)
(set-option :produce-unsat-cores true)
(set-option :simplify-interpolants true)
(set-logic QF_UFLIRA)
(set-option :verbosity 2)
(declare-fun |$b[0][0]| () Int)
(declare-fun |$b[0][1]| () Int)
(declare-fun |$b[0][2]| () Int)
(declare-fun |$b[0][3]| () Int)
(declare-fun |$b[0][4]| () Int)

agacek

(set-logic QF_UFLIRA)
(set-option :verbosity 2)
(define-fun T ((%init Bool) ($x$0 Real) ($y$0 Int) ($ok1$0 Bool) ($ok2$0 Bool) ($x$1 Real) ($y$1 Int) ($ok1$1 Bool) ($ok2$1 Bool)) Bool (and (= $ok1$1 (= (div $y$1 5) (to_int (/ (to_real $y$1) (/ 50 10))))) (= $ok2$1 (= (div (to_int $x$1) 5) (to_int (/ $x$1 (/ 50 10)))))))
(declare-fun %init () Bool)
(declare-fun $x$~1 () Real)
(declare-fun $y$~1 () Int)
(declare-fun $ok1$~1 () Bool)
(declare-fun $ok2$~1 () Bool)
(declare-fun $x$0 () Real)
(declare-fun $y$0 () Int)

agacek

type FGS__Guidance_Commands__Guidance_Commands_Impl = struct {Pitch_Delta : real; Pitch_Valid : bool};
type FGS__Lateral_Modes__Lateral_Modes_Impl = struct {HDG_active : bool; ROLL_active : bool};
type FGS__Flight_Modes__Flight_Modes_Impl = struct {active : bool; lat : FGS__Lateral_Modes__Lateral_Modes_Impl; ver : int};
type FGS__Guidance_Data__Guidance_Data_Impl = struct {cmds : FGS__Guidance_Commands__Guidance_Commands_Impl; mds : FGS__Flight_Modes__Flight_Modes_Impl};
type LDS__Leader_Selection_Data__Leader_Selection_Data_Impl = struct {Leader : int; Valid : bool};
type APS__Control_Surface_Actuator_Data__Control_Surface_Actuator_Data_Impl = struct {CSA_Pitch_Delta : real; CSA_Pitch_Valid : bool};
type ADS__Airspeed__Airspeed_Impl = struct {Val : real; Valid : bool};
type ADS__Pitch__Pitch_Impl = struct {Val : real; Valid : bool};
type ADS__Air_Data__Air_Data_Impl = struct {AirSpeed : ADS__Airspeed__Airspeed_Impl; Pitch : ADS__Pitch__Pitch_Impl};

agacek

type DATA_TYPES__NumActuators__impl = struct {AILL : int; AILR : int; BRAKE : int; ELLIB : int; ELLOB : int; ELRIB : int; ELROB : int; FLAPLI : int; FLAPLO : int; FLAPRI : int; FLAPRO : int; GEAR : int; RUDLO : int; RUDUP : int; SPLLIB : int; SPLLOB : int; SPLRIB : int; SPLROB : int; STEER : int; THROTL : int; THROTR : int};
type DATA_TYPES__BoolActuators__impl = struct {AILL : bool; AILR : bool; BRAKE : bool; ELLIB : bool; ELLOB : bool; ELRIB : bool; ELROB : bool; FLAPLI : bool; FLAPLO : bool; FLAPRI : bool; FLAPRO : bool; GEAR : bool; RUDLO : bool; RUDUP : bool; SPLLIB : bool; SPLLOB : bool; SPLRIB : bool; SPLROB : bool; STEER : bool; THROTL : bool; THROTR : bool};
type DATA_TYPES__Actuators__impl = struct {AILL : real; AILR : real; BRAKE : real; ELLIB : real; ELLOB : real; ELRIB : real; ELROB : real; FLAPLI : real; FLAPLO : real; FLAPRI : real; FLAPRO : real; GEAR : real; RUDLO : real; RUDUP : real; SPLLIB : real; SPLLOB : real; SPLRIB : real; SPLROB : real; STEER : real; THROTL : real; THROTR : real};

no