From beafef8f59b89d3c98d811c3f1cba7eadab29916 Mon Sep 17 00:00:00 2001
From: Jakub Janaszkiewicz <janaszkiewicz.jakub@gmail.com>
Date: Tue, 11 Apr 2023 11:56:00 +0200
Subject: [PATCH] Fix after rebase

---
 native-verifier/src/fol.rs     | 6 +++---
 native-verifier/src/smt_lib.rs | 3 ++-
 viper/src/verifier.rs          | 3 +++
 vir/defs/low/ast/expression.rs | 1 +
 4 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/native-verifier/src/fol.rs b/native-verifier/src/fol.rs
index 1d77b81c5cb..970bf206aa3 100644
--- a/native-verifier/src/fol.rs
+++ b/native-verifier/src/fol.rs
@@ -114,12 +114,12 @@ fn vir_statement_to_fol_statements(
                         position: op.position,
                     }),
                     Expression::UnaryOp(op) => Expression::UnaryOp(UnaryOp {
-                        op_kind: op.op_kind.clone(), // TODO: Copy trait derivation
+                        op_kind: op.op_kind,
                         argument: Box::new(substitute(&op.argument, mapping)),
                         position: op.position,
                     }),
                     Expression::ContainerOp(op) => Expression::ContainerOp(ContainerOp {
-                        kind: op.kind.clone(), // TODO: Copy trait derivation
+                        kind: op.kind,
                         container_type: op.container_type.clone(),
                         operands: op
                             .operands
@@ -163,7 +163,7 @@ fn vir_statement_to_fol_statements(
             preconds.chain(postconds).collect::<Vec<_>>()
         }
         Statement::Comment(comment) => vec![FolStatement::Comment(comment.comment.clone())],
-        Statement::LogEvent(_) => vec![], // TODO: Embed in SMT-LIB code
+        Statement::LogEvent(_) => vec![], // ignored
         _ => {
             unimplemented!("Statement {:?} not yet supported", statement);
         }
diff --git a/native-verifier/src/smt_lib.rs b/native-verifier/src/smt_lib.rs
index 6093eca47b4..b8771419c2e 100644
--- a/native-verifier/src/smt_lib.rs
+++ b/native-verifier/src/smt_lib.rs
@@ -303,7 +303,8 @@ impl SMTTranslatable for Program {
         self.domains.iter().for_each(|d| d.build_smt(smt));
         self.methods.iter().for_each(|d| d.build_smt(smt));
         self.procedures.iter().for_each(|d| d.build_smt(smt));
-        // TODO: Everything else
+        debug_assert!(self.functions.len() == 0); // TODO: Implement
+        debug_assert!(self.predicates.len() == 0);
     }
 }
 
diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs
index 2e006abf5bb..f38568e6d1f 100644
--- a/viper/src/verifier.rs
+++ b/viper/src/verifier.rs
@@ -69,6 +69,9 @@ impl<'a> Verifier<'a> {
                     VerificationBackend::Carbon => {
                         carbon::CarbonFrontend::with(env).new(reporter, logger)
                     }
+                    VerificationBackend::Lithium => {
+                        unreachable!("Lithium is not a JVM-based backend")
+                    }
                 }
             };
             let frontend_instance = jni.unwrap_result(unwrapped_frontend_instance);
diff --git a/vir/defs/low/ast/expression.rs b/vir/defs/low/ast/expression.rs
index 62076a9b5b6..d8148d235ef 100644
--- a/vir/defs/low/ast/expression.rs
+++ b/vir/defs/low/ast/expression.rs
@@ -175,6 +175,7 @@ pub struct ContainerOp {
     pub position: Position,
 }
 
+#[derive(Copy)]
 pub enum ContainerOpKind {
     SeqEmpty,
     SeqConstructor,