diff --git a/prusti-server/src/backend.rs b/prusti-server/src/backend.rs index ecb3b81297e..8bb63a744d1 100644 --- a/prusti-server/src/backend.rs +++ b/prusti-server/src/backend.rs @@ -4,7 +4,7 @@ use prusti_common::{ vir::{LoweringContext, ToViper}, Stopwatch, }; -use viper::{VerificationContext, VerificationResult}; +use viper::VerificationContext; pub enum Backend<'a> { Viper(viper::Verifier<'a>, &'a VerificationContext<'a>), @@ -37,7 +37,10 @@ impl<'a> Backend<'a> { viper.verify(viper_program) }) } - Backend::Lithium(lithium) => lithium.verify(program), + Backend::Lithium(lithium) => { + Stopwatch::start("prusti-server", "verifierication"); + lithium.verify(program) + } } } } diff --git a/prusti-server/src/process_verification.rs b/prusti-server/src/process_verification.rs index 883aee66929..0a9defd4295 100644 --- a/prusti-server/src/process_verification.rs +++ b/prusti-server/src/process_verification.rs @@ -110,11 +110,11 @@ pub fn process_verification_request<'v, 't: 'v>( ), verification_context, ), - VerificationBackend::Lithium => { - Backend::Lithium(native_verifier::Verifier::new(config::smt_solver_path())) - // TODO: Wrapper support - } - }; + VerificationBackend::Lithium => { + Backend::Lithium(native_verifier::Verifier::new(config::smt_solver_path())) + // TODO: SMT Wrapper support + } + }; stopwatch.start_next("backend verification"); let mut result = backend.verify(&request.program);