another unsafe core proof workaround for trait resolution

prusti-interface/src/environment/mod.rs

@@ -523,10 +523,18 @@ impl<'tcx> Environment<'tcx> {
         called_def_id: ProcedureDefId, // what are we calling?
         call_substs: SubstsRef<'tcx>,
     ) -> (ProcedureDefId, SubstsRef<'tcx>) {
+        use prusti_rustc_interface::middle::ty::TypeVisitable;
+
         // Avoids a compiler-internal panic
         // this check ignores any lifetimes/regions, which at this point would
         // need inference. They are thus ignored.
-        if self.any_type_needs_infer(call_substs) {
+        // TODO: different behaviour used for unsafe core proof
+        let needs_infer = if config::unsafe_core_proof() {
+            call_substs.needs_infer()
+        } else {
+            self.any_type_needs_infer(call_substs)
+        };
+        if needs_infer {
             return (called_def_id, call_substs);
         }
 

viper/src/silicon_counterexample.rs

@@ -222,8 +222,9 @@ fn unwrap_model_entry<'a>(
         }
         "viper.silicon.reporting.LitPermEntry" => {
             let lit_perm_wrapper = silicon::reporting::LitPermEntry::with(env);
-            let value = jni.unwrap_result(lit_perm_wrapper.call_value(entry));
-            Some(ModelEntry::LitPerm(value.to_string()))
+            let value_scala = jni.unwrap_result(lit_perm_wrapper.call_value(entry));
+            let value = jni.to_string(value_scala);
+            Some(ModelEntry::LitPerm(value))
         }
         "viper.silicon.reporting.RefEntry" => {
             let ref_wrapper = silicon::reporting::RefEntry::with(env);