Option updates

exps/chc-comp-2020/smv/chc-LIA-lin-arrays_000.smv

@@ -0,0 +1,109 @@
+-- generated by vmt2nuxmv.py on Fri Feb 26 09:43:50 2021
+MODULE main
+VAR
+".loc.10" : boolean;
+".loc.9" : boolean;
+".y.8" : integer;
+"A_3" : integer;
+"D_3" : integer;
+"E_3" : integer;
+"F_3" : array integer of integer;
+"G_3" : integer;
+
+DEFINE
+__expr1 := ! ".loc.10";
+__expr2 := ! ".loc.9";
+__expr3 := __expr2 & __expr1;
+__expr4 := "G_3" <= 0;
+__expr5 := ! __expr4;
+__expr6 := "E_3" <= 0;
+__expr7 := __expr6 | __expr5;
+__expr8 := ! __expr6;
+__expr9 := __expr8 & __expr7;
+__expr10 := ".loc.9" & __expr9;
+__expr11 := next(".loc.9") & __expr10;
+__expr12 := __expr1 & __expr11;
+__expr13 := "E_3" = next("E_3");
+__expr14 := __expr13 & __expr12;
+__expr15 := ! next(".loc.10");
+__expr16 := __expr15 & __expr14;
+__expr17 := -1 * next(".y.8");
+__expr18 := ".y.8" + __expr17;
+__expr19 := __expr18 = -1;
+__expr20 := __expr19 & __expr16;
+__expr21 := WRITE("F_3", "G_3", 0);
+__expr22 := next("F_3") = __expr21;
+__expr23 := __expr22 & __expr20;
+__expr24 := -1 * "G_3";
+__expr25 := ".y.8" + __expr24;
+__expr26 := "E_3" + __expr25;
+__expr27 := __expr26 = 0;
+__expr28 := __expr27 & __expr23;
+__expr29 := "D_3" <= ".y.8";
+__expr30 := ! __expr29;
+__expr31 := __expr30 & __expr28;
+__expr32 := "D_3" = next("D_3");
+__expr33 := __expr32 & __expr31;
+__expr34 := __expr2 & __expr5;
+__expr35 := next(".loc.9") & __expr34;
+__expr36 := __expr1 & __expr35;
+__expr37 := __expr36 & __expr15;
+__expr38 := next(".y.8") = 0;
+__expr39 := __expr38 & __expr37;
+__expr40 := next("E_3") <= 0;
+__expr41 := ! __expr40;
+__expr42 := __expr41 & __expr39;
+__expr43 := next("D_3") <= -1;
+__expr44 := ! __expr43;
+__expr45 := __expr44 & __expr42;
+__expr46 := next("D_3") <= "G_3";
+__expr47 := __expr46 & __expr45;
+__expr48 := READ("F_3", "G_3");
+__expr49 := __expr48 <= -1;
+__expr50 := ! __expr49;
+__expr51 := "D_3" + __expr24;
+__expr52 := "E_3" + __expr51;
+__expr53 := __expr52 = 0;
+__expr54 := __expr53 & __expr8;
+__expr55 := "A_3" <= "D_3";
+__expr56 := ! __expr55;
+__expr57 := __expr56 & __expr54;
+__expr58 := __expr57 & __expr7;
+__expr59 := __expr58 & __expr50;
+__expr60 := ".loc.10" & __expr59;
+__expr61 := __expr2 & __expr60;
+__expr62 := ! next(".loc.9");
+__expr63 := __expr62 & __expr61;
+__expr64 := __expr13 & __expr63;
+__expr65 := "F_3" = next("F_3");
+__expr66 := __expr65 & __expr64;
+__expr67 := -1 * next("D_3");
+__expr68 := "D_3" + __expr67;
+__expr69 := __expr68 = -1;
+__expr70 := __expr69 & __expr66;
+__expr71 := "A_3" = next("A_3");
+__expr72 := __expr71 & __expr70;
+__expr73 := ".loc.9" & __expr62;
+__expr74 := __expr1 & __expr73;
+__expr75 := next("D_3") = 0;
+__expr76 := __expr75 & __expr74;
+__expr77 := __expr76 & __expr29;
+__expr78 := __expr77 & __expr13;
+__expr79 := __expr78 & __expr65;
+__expr80 := "D_3" = next("A_3");
+__expr81 := __expr80 & __expr79;
+__expr82 := __expr49 & __expr58;
+__expr83 := ".loc.10" & __expr82;
+__expr84 := __expr2 & __expr83;
+__expr85 := __expr84 & next(".loc.9");
+__expr86 := __expr85 | __expr81;
+__expr87 := __expr86 | __expr72;
+__expr88 := __expr87 & next(".loc.10");
+__expr89 := __expr88 | __expr47;
+__expr90 := __expr89 | __expr33;
+__expr91 := ".loc.9" & ".loc.10";
+__expr92 := ! __expr91;
+
+INIT __expr3;
+TRANS __expr90;
+INVARSPEC __expr92;