input OTHER step

kroening · kroening · commit c074b45427dd · 2016-07-11T19:57:04.000+01:00
diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp
@@ -1041,6 +1041,10 @@ void path_symext::operator()(
       {
         // ignore for SC
       }
+      else if(statement==ID_input)
+      {
+        // just needs to be recorded
+      }
       else
         throw "unexpected OTHER statement: "+id2string(statement);
     }

Original file line number	Diff line number	Diff line change
`@@ -1041,6 +1041,10 @@ void path_symext::operator()(`
`1041`	`1041`	`{`
`1042`	`1042`	`// ignore for SC`
`1043`	`1043`	`}`
	`1044`	`+ else if(statement==ID_input)`
	`1045`	`+ {`
	`1046`	`+ // just needs to be recorded`
	`1047`	`+ }`
`1044`	`1048`	`else`
`1045`	`1049`	`throw "unexpected OTHER statement: "+id2string(statement);`
`1046`	`1050`	`}`