From fa253fcf9130dab64e4ff4da2a0d6ec65c48ccb5 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Date: Wed, 23 Dec 2020 19:54:36 +0100
Subject: [PATCH] Use default solver in CBMC proof for
 aws_cryptosdk_keyring_trace_copy_all (#677)

* Restore YAML file for `aws_cryptosdk_keyring_trace_copy_all` proof

* Unset external SAT solver for aws_cryptosdk_keyring_trace_copy_all proof
---
 .../proofs/aws_cryptosdk_keyring_trace_copy_all/Makefile     | 5 +++++
 .../aws_cryptosdk_keyring_trace_copy_all/cbmc-batch.yaml     | 4 ++++
 2 files changed, 9 insertions(+)
 create mode 100644 verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/cbmc-batch.yaml

diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/Makefile b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/Makefile
index 6d2c1d203..abdcaa3a4 100644
--- a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/Makefile
+++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/Makefile
@@ -33,6 +33,11 @@ CBMCFLAGS +=
 DEFINES += -DAWS_NO_STATIC_IMPL
 DEFINES += -DNUM_ELEMS=$(NUM_ELEMS)
 
+# Running this proof with kissat causes it to fail due to kissat
+# getting an "out of memory" error - even if only this proof is running
+# It does not happen with the default solver, so we unset the variable here
+EXTERNAL_SAT_SOLVER =
+
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/array_list.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/byte_buf.c
 PROJECT_SOURCES += $(CBMC_ROOT)/aws-c-common/source/common.c
diff --git a/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/cbmc-batch.yaml b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/cbmc-batch.yaml
new file mode 100644
index 000000000..e936b4599
--- /dev/null
+++ b/verification/cbmc/proofs/aws_cryptosdk_keyring_trace_copy_all/cbmc-batch.yaml
@@ -0,0 +1,4 @@
+:
+  This file marks this directory as containing a CBMC proof. This file
+  is automatically clobbered in CI and replaced with parameters for
+  running the proof.
\ No newline at end of file