agacek

node integ(x : int) returns (sum : int);
let
  sum = x + (0 -> pre sum);
tel;

node main(x : int; y : int) returns (z : int);
var
  history : bool;
  prop : bool;
let

agacek

node main(
  a : bool;
  b : bool;
  c : bool;
  d : bool
) returns (
  cost : int
);
var
  torch : bool;

agacek

node integ(x : int) returns (sum : int);
let
  sum = x + (0 -> pre sum);
tel;

node main(x : int; y : int; r : real) returns (z : int);
var
  history : bool;
  prop1 : bool;
  prop2 : bool;

agacek

-- This file has one property which is false with K = 25

-- The peg swap puzzle. You have have the following board
--  B B B B . R R R R
-- Where B is a blue peg, R is a red peg, and . is empty.
-- Blue pegs only move right. Red pegs only move left.
-- A peg can move to an empty space next to it,
-- or hop over a single peg next to it into an empty space.
-- The game is won if you can reach the configuration:
--  R R R R . B B B B

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

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

(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

(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

(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

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;