Fix after rebase

viperproject · Feb 27, 2023 · 096bdd5 · 096bdd5
1 parent bf396ca
commit 096bdd5
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 7 deletions.
diff --git 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
@@ -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);