@@ -62,10 +62,7 @@ procedure Procedure(y: int)
6262 Parser . Parse ( programString , "fakeFilename10" , out var program ) ;
6363 var options = CommandLineOptions . FromArguments ( TextWriter . Null ) ;
6464 var engine = ExecutionEngine . CreateWithoutSharedCache ( options ) ;
65- Assert . Throws < ArgumentException > ( ( ) =>
66- {
67- var tasks = engine . GetVerificationTasks ( program ) ;
68- } ) ;
65+ Assert . ThrowsAsync < ArgumentException > ( ( ) => engine . GetVerificationTasks ( program ) ) ;
6966 }
7067
7168 [ Test ]
@@ -80,10 +77,7 @@ procedure Procedure(y: int)
8077 Parser . Parse ( programString , "fakeFilename10" , out var program ) ;
8178 var options = CommandLineOptions . FromArguments ( TextWriter . Null ) ;
8279 var engine = ExecutionEngine . CreateWithoutSharedCache ( options ) ;
83- Assert . Throws < ArgumentException > ( ( ) =>
84- {
85- var tasks = engine . GetVerificationTasks ( program ) ;
86- } ) ;
80+ Assert . ThrowsAsync < ArgumentException > ( ( ) => engine . GetVerificationTasks ( program ) ) ;
8781 }
8882
8983 [ Test ]
@@ -102,7 +96,7 @@ procedure Procedure(y: int)
10296 options . VcsSplitOnEveryAssert = true ;
10397 options . PrintErrorModel = 1 ;
10498 var engine = ExecutionEngine . CreateWithoutSharedCache ( options ) ;
105- var tasks = engine . GetVerificationTasks ( program ) ;
99+ var tasks = await engine . GetVerificationTasks ( program ) ;
106100
107101 // The first split is empty. Maybe it can be optimized away
108102 Assert . AreEqual ( 5 , tasks . Count ) ;
@@ -133,7 +127,7 @@ procedure Second(y: int)
133127 var options = CommandLineOptions . FromArguments ( TextWriter . Null ) ;
134128 options . PrintErrorModel = 1 ;
135129 var engine = ExecutionEngine . CreateWithoutSharedCache ( options ) ;
136- var tasks = engine . GetVerificationTasks ( program ) ;
130+ var tasks = await engine . GetVerificationTasks ( program ) ;
137131 Assert . AreEqual ( 2 , tasks . Count ) ;
138132 Assert . NotNull ( tasks [ 0 ] . Split . Implementation ) ;
139133 var result1 = await tasks [ 0 ] . TryRun ( ) ! . ToTask ( ) ;
@@ -292,7 +286,7 @@ procedure Foo(x: int) {
292286}" . TrimStart ( ) ;
293287 var result = Parser . Parse ( source , "fakeFilename1" , out var program ) ;
294288 Assert . AreEqual ( 0 , result ) ;
295- var tasks = engine . GetVerificationTasks ( program ) [ 0 ] ;
289+ var tasks = ( await engine . GetVerificationTasks ( program ) ) [ 0 ] ;
296290 var statusList1 = new List < IVerificationStatus > ( ) ;
297291 var firstStatuses = tasks . TryRun ( ) ! ;
298292 await firstStatuses . Where ( s => s is Running ) . FirstAsync ( ) . ToTask ( ) ;
@@ -328,7 +322,7 @@ procedure Foo(x: int) {
328322}" . TrimStart ( ) ;
329323 var result = Parser . Parse ( source , "fakeFilename1" , out var program ) ;
330324 Assert . AreEqual ( 0 , result ) ;
331- var task = engine . GetVerificationTasks ( program ) [ 0 ] ;
325+ var task = ( await engine . GetVerificationTasks ( program ) ) [ 0 ] ;
332326 var statusList1 = new List < IVerificationStatus > ( ) ;
333327 var firstStatuses = task . TryRun ( ) ! ;
334328 var runDuringRun1 = task . TryRun ( ) ;
@@ -372,7 +366,7 @@ public async Task FromSeedResetsState() {
372366}" . TrimStart ( ) ;
373367 Parser . Parse ( source , "fakeFilename1" , out var program ) ;
374368 Assert . AreEqual ( "Bad" , program . Implementations . ElementAt ( 0 ) . Name ) ;
375- var tasks = engine . GetVerificationTasks ( program ) ;
369+ var tasks = await engine . GetVerificationTasks ( program ) ;
376370 var task = tasks [ 0 ] ;
377371 await task . TryRun ( ) ! . ToTask ( ) ;
378372 var secondResult = task . FromSeed ( 100 ) . TryRun ( ) ! ;
@@ -402,7 +396,7 @@ public async Task StatusTest() {
402396" ;
403397 Parser . Parse ( programString , "fakeFilename1" , out var program ) ;
404398 Assert . AreEqual ( "Bad" , program . Implementations . ElementAt ( 0 ) . Name ) ;
405- var tasks = engine . GetVerificationTasks ( program ) ;
399+ var tasks = await engine . GetVerificationTasks ( program ) ;
406400 var statusList = new List < ( string , IVerificationStatus ) > ( ) ;
407401
408402 var first = tasks [ 0 ] ;
@@ -472,11 +466,13 @@ public async Task SolverCrash()
472466 // We limit the number of checkers to 1.
473467 options . VcsCores = 1 ;
474468
475- var outcome1 = await executionEngine . GetVerificationTasks ( terminatingProgram ) [ 0 ] . TryRun ( ) ! . ToTask ( ) ;
476- Assert . IsTrue ( outcome1 is Completed completed && completed . Result . Outcome == SolverOutcome . Undetermined ) ;
469+ var tasks1 = await executionEngine . GetVerificationTasks ( terminatingProgram ) ;
470+ var outcome1 = await tasks1 [ 0 ] . TryRun ( ) ! . ToTask ( ) ;
471+ Assert . IsTrue ( outcome1 is Completed { Result . Outcome : SolverOutcome . Undetermined } ) ;
477472 options . CreateSolver = ( _ , _ ) => new UnsatSolver ( ) ;
478- var outcome2 = await executionEngine . GetVerificationTasks ( terminatingProgram ) [ 0 ] . TryRun ( ) ! . ToTask ( ) ;
479- Assert . IsTrue ( outcome2 is Completed completed2 && completed2 . Result . Outcome == SolverOutcome . Valid ) ;
473+ var tasks2 = await executionEngine . GetVerificationTasks ( terminatingProgram ) ;
474+ var outcome2 = await tasks2 [ 0 ] . TryRun ( ) ! . ToTask ( ) ;
475+ Assert . IsTrue ( outcome2 is Completed { Result . Outcome : SolverOutcome . Valid } ) ;
480476 }
481477
482478 [ Test ]
0 commit comments