Merge pull request #319 from ethereum/smtchecker-tests

Add SMTChecker smoke tests
ethereum · Dec 12, 2018 · 1af3817 · 1af3817
2 parents d3b6848 + fbc7378
commit 1af3817
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 0 deletions.
diff --git a/test/index.js b/test/index.js
@@ -3,6 +3,7 @@ const semver = require('semver');
 require('./linker.js');
 require('./translate.js');
 require('./package.js');
+require('./smtchecker.js');
 require('./abi.js');
 require('./determinism.js');
 

diff --git a/test/smtchecker.js b/test/smtchecker.js
@@ -0,0 +1,18 @@
+const tape = require('tape');
+const smtchecker = require('../smtchecker.js');
+
+tape('SMTChecker', function (t) {
+  t.test('smoke test with no axuiliaryInputRequested', function (st) {
+    var input = {};
+    var output = {};
+    st.equal(smtchecker.handleSMTQueries(input, output), null);
+    st.end();
+  });
+
+  t.test('smoke test with no smtlib2queries', function (st) {
+    var input = {};
+    var output = { auxiliaryInputRequested: {} };
+    st.equal(smtchecker.handleSMTQueries(input, output), null);
+    st.end();
+  });
+});