View difference between Paste ID: KiwFJTrK and Fc1nEcb2

-; generated by the as2smt translator
+
 
 (set-logic QF_LIA)
 
 ; initial variable declarations
 
 (declare-fun var1 () Int)
 (assert     (and
       (>= var1 0)
       (<= var1 7)
     ))
 (declare-fun var1_post () Int)
 (assert     (and
       (>= var1_post 0)
       (<= var1_post 7)
     ))
 (declare-fun var2 () Int)
 (assert     (and
       (>= var2 0)
       (<= var2 4)
     ))
 (declare-fun var2_post () Int)
 (assert     (and
       (>= var2_post 0)
       (<= var2_post 4)
     ))
 (declare-fun var3 () Int)
 (assert     (and
       (>= var3 0)
       (<= var3 4)
     ))
 (declare-fun var3_post () Int)
 (assert     (and
       (>= var3_post 0)
       (<= var3_post 4)
     ))
 (declare-fun var4 () Int)
 (assert     (and
       (>= var4 0)
       (<= var4 1)
     ))
 (declare-fun var4_post () Int)
 (assert     (and
       (>= var4_post 0)
       (<= var4_post 1)
     ))
 
 (assert (not
 (and
-; negated specification
+
     var1
     7
   )
   (=
     var2
     0
   )
   (=
     var1_post
     2
   )
   (=
     var4_post
     1
   )
   (=
     var2_post
       var2
   )
   (=
     var3_post
       var3
   )
 )
 ))
 
 (assert
   (and
     (=
       var1
-; mutant
+
     )
     (=
 	var2
       0
     )
     (=
       var1_post
       2
     )
     (=
       var4_post
       1
     )
     (=
       var2_post
 	var2
     )
     (=
       var3_post
 	var3
     )
 
   )
 )
 
 ; start check
 (check-sat)
 (get-model)
 (exit)