diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-03-16 12:17:43 -0700 |
|---|---|---|
| committer | Alex Ozdemir <aozdemir@hmc.edu> | 2020-03-16 16:52:50 -0700 |
| commit | 905d77664cdedb5d1f3fec91c32c5033a0618e67 (patch) | |
| tree | 0d1421454b9208d4cca68d7e9edb13072afce8f0 /src/proof | |
| parent | 53a07d0331d71656904a7333b5ed0c835d7d4c38 (diff) | |
Only save farkas+tightening proofs. Error on holes
I'll remove the error later
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/arith_proof.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index 7deb22d48..2660f723f 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -1156,8 +1156,10 @@ void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma, } else { + AlwaysAssert(false) << "arith hole!"; os << "\n; Arithmetic proofs which use reasoning more complex than Farkas " - "proofs are currently unsupported\n(clausify_false trust)\n"; + "proofs and bound tightening are currently unsupported\n" + "(clausify_false trust)\n"; } } |