diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2018-06-13 11:19:03 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2018-06-13 11:19:03 -0500 |
| commit | d135cafa234a5c36278b3ee9b748b7dc65459794 (patch) | |
| tree | 12311c284f638842b007f10921b0199dbac02d7c | |
| parent | ce028b357db6a8d2bcfdc24fad1cac7a69537f4a (diff) | |
Add regression
| -rw-r--r-- | src/theory/evaluator.cpp | 1 | ||||
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/t8.sy | 31 |
3 files changed, 32 insertions, 1 deletions
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index a220d7703..0f7d80234 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -239,7 +239,6 @@ EvalResult Evaluator::evalInternal(TNode n, { Trace("evaluator") << "Kind " << currNodeVal.getKind() << " not supported" << std::endl; - results[currNode] = EvalResult(); return EvalResult(); } } diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 0e1c8e2cf..9a09c57ec 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1537,6 +1537,7 @@ REG1_TESTS = \ regress1/sygus/strings-trivial.sy \ regress1/sygus/sygus-dt.sy \ regress1/sygus/sygus-uf-ex.sy \ + regress1/sygus/t8.sy \ regress1/sygus/tl-type-0.sy \ regress1/sygus/tl-type-4x.sy \ regress1/sygus/tl-type.sy \ diff --git a/test/regress/regress1/sygus/t8.sy b/test/regress/regress1/sygus/t8.sy new file mode 100644 index 000000000..4dd726875 --- /dev/null +++ b/test/regress/regress1/sygus/t8.sy @@ -0,0 +1,31 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) +( +synth-fun f_143-17-143-55 ( (x2 Int) (x1 Int) (parentNode Int) (EMPTY_PARENT Int)) Bool + ((Start Bool ( +(< IntExpr IntExpr) +(and Start Start) +(= IntExpr IntExpr) +(not Start ) +(<= IntExpr IntExpr) +(or Start Start) + + + +)) +(IntExpr Int ( +x2 x1 parentNode EMPTY_PARENT +0 1 +)) + + ) +) +(declare-var x2_143-17-143-55 Int) +(declare-var x1_143-17-143-55 Int) +(declare-var parentNode_143-17-143-55 Int) +(declare-var EMPTY_PARENT_143-17-143-55 Int) + +(constraint (=> (and (= parentNode_143-17-143-55 0) (and (= EMPTY_PARENT_143-17-143-55 -1) (and (= x2_143-17-143-55 1) (= x1_143-17-143-55 1)) ) ) (= (f_143-17-143-55 x2_143-17-143-55 x1_143-17-143-55 parentNode_143-17-143-55 EMPTY_PARENT_143-17-143-55 ) true))) + +(check-synth) |