diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-06 14:27:10 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-06 14:27:10 -0600 |
commit | 89337334236176bff2d561c42b9b55ab9d91bd62 (patch) | |
tree | a7ca068313b3625865bedc425a9607b814e5868e /test/regress/regress2 | |
parent | b9347f7d0ca130f85df103e5271536a165a04a64 (diff) |
Remove tester name from APIs (#3929)
This removes the field "tester name" from the Expr-level and Term-level APIs. This field is an artifact of parsing and thus should be handled in the parsers.
This refactor uncovered an issue in our regressions, namely our smt version >= 2.6 was not strictly complaint, since the symbol is-cons was being automatically defined for testers of constructors cons. This disables this behavior when strict mode is enabled. It updates the regressions with this issue.
This is work towards parser migration.
Diffstat (limited to 'test/regress/regress2')
-rw-r--r-- | test/regress/regress2/bug674.smt2 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress2/bug674.smt2 b/test/regress/regress2/bug674.smt2 index fccde862a..31eaa5aba 100644 --- a/test/regress/regress2/bug674.smt2 +++ b/test/regress/regress2/bug674.smt2 @@ -1,8 +1,8 @@ ; COMMAND-LINE: --quant-ind --incremental --rewrite-divk (set-logic ALL_SUPPORTED) (declare-datatypes ((Lst 0)) (((cons (head Int) (tail Lst)) (nil)))) -(define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite (is-nil l1) l2 (cons (head l1) (app (tail l1) l2)))) -(define-fun-rec rev ((l Lst)) Lst (ite (is-nil l) nil (app (rev (tail l)) (cons (head l) nil)))) +(define-fun-rec app ((l1 Lst) (l2 Lst)) Lst (ite ((_ is nil) l1) l2 (cons (head l1) (app (tail l1) l2)))) +(define-fun-rec rev ((l Lst)) Lst (ite ((_ is nil) l) nil (app (rev (tail l)) (cons (head l) nil)))) ; EXPECT: unsat (push 1) (assert (not (=> true (and (forall (($l1$0 Lst) ($l2$0 Lst) ($l3$0 Lst)) (= (app $l1$0 (app $l2$0 $l3$0)) (app (app $l1$0 $l2$0) $l3$0))))))) |