cvc5.git
11 years agofixed bug520
Liana Hadarean [Tue, 16 Jul 2013 22:20:09 +0000 (17:20 -0500)]
fixed bug520

11 years agoFix for get-antlr script and PIC/non-PIC objects, on some platforms
Morgan Deters [Tue, 16 Jul 2013 17:42:30 +0000 (13:42 -0400)]
Fix for get-antlr script and PIC/non-PIC objects, on some platforms

11 years ago"Tabular"-style function definitions in models with --no-condense-function-values
Morgan Deters [Tue, 16 Jul 2013 21:29:42 +0000 (17:29 -0400)]
"Tabular"-style function definitions in models with --no-condense-function-values

11 years agoMinor bugfixes to model-building
Morgan Deters [Tue, 16 Jul 2013 21:29:30 +0000 (17:29 -0400)]
Minor bugfixes to model-building

11 years agoRemove now-unused language bindings interface file.
Morgan Deters [Sat, 13 Jul 2013 15:19:53 +0000 (11:19 -0400)]
Remove now-unused language bindings interface file.

11 years agoFix language bindings and portfolio builds.
Morgan Deters [Sat, 13 Jul 2013 15:04:10 +0000 (11:04 -0400)]
Fix language bindings and portfolio builds.

11 years agoFix for curious GCC 4.8 translation with -O.
Morgan Deters [Fri, 12 Jul 2013 22:18:07 +0000 (18:18 -0400)]
Fix for curious GCC 4.8 translation with -O.

11 years agoRemove auto-aritization from TPTP parser
Morgan Deters [Wed, 10 Jul 2013 19:05:41 +0000 (15:05 -0400)]
Remove auto-aritization from TPTP parser

11 years agoSupport for TPTP's TFF0 (with arithmetic)
Morgan Deters [Mon, 24 Jun 2013 23:58:37 +0000 (19:58 -0400)]
Support for TPTP's TFF0 (with arithmetic)

This commit reverses an "SZS ontology compliance hack" that was
done for CASC-24 this year, and adds a TPTP pretty-printer which
is capable of outputting results in the TPTP way (rather than the
SMT way).

This commit includes minor changes to the Expr package to add
obvious missing functionality, and to fix the way expressions
with builtin operators are made.  These changes are truly a
_fix_, the implementation had not been properly aligned with
the design vision for some corner cases.

11 years agoFix for Boolean-term rewriting and LAMBDAs
Morgan Deters [Thu, 11 Jul 2013 20:47:27 +0000 (16:47 -0400)]
Fix for Boolean-term rewriting and LAMBDAs

11 years agoFix for bug 519; don't involve ITESimplifier in model generation.
Morgan Deters [Wed, 10 Jul 2013 01:22:53 +0000 (21:22 -0400)]
Fix for bug 519; don't involve ITESimplifier in model generation.

11 years agoadd relevant domain computation
Andrew Reynolds [Tue, 9 Jul 2013 20:43:28 +0000 (15:43 -0500)]
add relevant domain computation

11 years agoModel output is now const; this related to bug 519
Morgan Deters [Sun, 7 Jul 2013 00:32:48 +0000 (20:32 -0400)]
Model output is now const; this related to bug 519

11 years agoFix for a datatype parsing bug that Tim found.
Morgan Deters [Fri, 5 Jul 2013 21:25:27 +0000 (17:25 -0400)]
Fix for a datatype parsing bug that Tim found.

11 years agoMake uf strong solver user-context dependent, fixes bug 522.
Andrew Reynolds [Tue, 2 Jul 2013 19:09:17 +0000 (14:09 -0500)]
Make uf strong solver user-context dependent, fixes bug 522.

11 years agoMinor fixes for bounded integers, rewrite engine.
Andrew Reynolds [Tue, 2 Jul 2013 18:40:26 +0000 (13:40 -0500)]
Minor fixes for bounded integers, rewrite engine.

11 years agoMore bug fixes for interval models.
Andrew Reynolds [Fri, 28 Jun 2013 20:46:13 +0000 (15:46 -0500)]
More bug fixes for interval models.

11 years agoFix portfolio builds after yesterday's commits.
Morgan Deters [Fri, 28 Jun 2013 13:09:47 +0000 (09:09 -0400)]
Fix portfolio builds after yesterday's commits.

11 years agoBetter check-models output for some kinds of problems; add anassertion that the maste...
Morgan Deters [Thu, 27 Jun 2013 22:39:20 +0000 (18:39 -0400)]
Better check-models output for some kinds of problems; add anassertion that the master equality engine is consistent when it needs to be.

This is intended to help root out some recent model-generation bugs.

11 years agoFix minor warnings found by recent clang/gcc.
Morgan Deters [Thu, 27 Jun 2013 21:06:56 +0000 (17:06 -0400)]
Fix minor warnings found by recent clang/gcc.

11 years agoRemove output.h from public space, to avoid clashes with symbols defined in users...
Morgan Deters [Thu, 27 Jun 2013 19:35:24 +0000 (15:35 -0400)]
Remove output.h from public space, to avoid clashes with symbols defined in users' space.

Specifically, output.h was moved to CVC4's "private-library" rules, which means that it's
not installed on users' machines, and public headers should not include it.

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.

11 years agoSmall fix for IS_INTEGER.
Morgan Deters [Thu, 27 Jun 2013 19:34:32 +0000 (15:34 -0400)]
Small fix for IS_INTEGER.

11 years agoRemove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they don't escape...
Morgan Deters [Thu, 27 Jun 2013 19:01:21 +0000 (15:01 -0400)]
Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they don't escape to user space

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.

11 years agoBetter user documentation for mkVar() and mkBoundVar().
Morgan Deters [Thu, 27 Jun 2013 18:55:55 +0000 (14:55 -0400)]
Better user documentation for mkVar() and mkBoundVar().

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.

11 years agoMinor printer cleanup for SMT-LIBv2 symbols "div" and "mod".
Morgan Deters [Thu, 27 Jun 2013 18:42:28 +0000 (14:42 -0400)]
Minor printer cleanup for SMT-LIBv2 symbols "div" and "mod".

Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.

11 years agoAdd support for interval models in bounded integers MBQI (in progress).
Andrew Reynolds [Wed, 26 Jun 2013 19:40:05 +0000 (14:40 -0500)]
Add support for interval models in bounded integers MBQI (in progress).

11 years agoMerge branch '1.2.x'
Morgan Deters [Tue, 25 Jun 2013 23:53:02 +0000 (19:53 -0400)]
Merge branch '1.2.x'

11 years agoProposed fix for bug #513
Morgan Deters [Tue, 25 Jun 2013 23:39:32 +0000 (19:39 -0400)]
Proposed fix for bug #513

11 years agoRefactoring of model engine to separate individual implementations of model builder...
Andrew Reynolds [Tue, 25 Jun 2013 17:18:05 +0000 (12:18 -0500)]
Refactoring of model engine to separate individual implementations of model builder.  Begin work on interval models for integers.  Other minor cleanup.

11 years agoAdd files missing from last commit
Morgan Deters [Tue, 25 Jun 2013 00:21:37 +0000 (20:21 -0400)]
Add files missing from last commit

11 years agoSupport for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk allows...
Morgan Deters [Mon, 24 Jun 2013 23:35:58 +0000 (19:35 -0400)]
Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk allows linearization of div,mod,/ by a constant.

11 years agoAdd options for symmetry breaking in uf+ss totality axiom approach, option for using...
Andrew Reynolds [Mon, 24 Jun 2013 17:52:07 +0000 (12:52 -0500)]
Add options for symmetry breaking in uf+ss totality axiom approach, option for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine

11 years agoFix failure in non-assertion builds on incorrect SmtEngine use.
Morgan Deters [Fri, 21 Jun 2013 15:15:57 +0000 (11:15 -0400)]
Fix failure in non-assertion builds on incorrect SmtEngine use.

11 years agoMerge branch '1.2.x'
Morgan Deters [Wed, 19 Jun 2013 22:28:38 +0000 (18:28 -0400)]
Merge branch '1.2.x'

11 years agoWorkaround for suspected clang 3.0 codegen bug on Mac
Morgan Deters [Wed, 19 Jun 2013 22:27:42 +0000 (18:27 -0400)]
Workaround for suspected clang 3.0 codegen bug on Mac

11 years agoFix to the "include" extended feature of the SMT-LIB parser
Morgan Deters [Wed, 19 Jun 2013 15:11:27 +0000 (11:11 -0400)]
Fix to the "include" extended feature of the SMT-LIB parser

11 years agoGive a more useful parse error message for "undeclared variable -1".
Morgan Deters [Wed, 19 Jun 2013 15:09:49 +0000 (11:09 -0400)]
Give a more useful parse error message for "undeclared variable -1".

Indeed, "-1" is a valid user symbol in SMT-LIB; this commit makes a small
change to the parser to detect when something like "-1" is used but
undeclared, and adds a note to the error message giving the syntax for
unary minus.

11 years agoJava streams example I forgot to add a long time ago
Morgan Deters [Mon, 17 Jun 2013 22:36:26 +0000 (18:36 -0400)]
Java streams example I forgot to add a long time ago

11 years agoMake --var-elim-quant true by default. Add rewrite engine to quantifiers module.
Andrew Reynolds [Mon, 17 Jun 2013 20:31:28 +0000 (15:31 -0500)]
Make --var-elim-quant true by default.  Add rewrite engine to quantifiers module.

11 years agoFix in SMT2 parser for parametric datatypes
Andrew Reynolds [Sun, 16 Jun 2013 02:00:39 +0000 (21:00 -0500)]
Fix in SMT2 parser for parametric datatypes

11 years agoanother fix for array-store-all printing
Morgan Deters [Mon, 10 Jun 2013 03:11:55 +0000 (23:11 -0400)]
another fix for array-store-all printing

11 years agoBetter array-store-all output for SMT-LIB.
Morgan Deters [Mon, 10 Jun 2013 02:40:23 +0000 (22:40 -0400)]
Better array-store-all output for SMT-LIB.

11 years agoFix typos in alttheoryskel
Morgan Deters [Sat, 8 Jun 2013 23:17:03 +0000 (19:17 -0400)]
Fix typos in alttheoryskel

11 years agoFixes for Boolean terms in arrays (including fix for bug 517).
Morgan Deters [Fri, 7 Jun 2013 15:30:00 +0000 (11:30 -0400)]
Fixes for Boolean terms in arrays (including fix for bug 517).

11 years agoOne more case for arrays of Boolean.
Morgan Deters [Fri, 7 Jun 2013 21:35:21 +0000 (17:35 -0400)]
One more case for arrays of Boolean.

11 years agoFix for bug 517.
Morgan Deters [Fri, 7 Jun 2013 15:30:00 +0000 (11:30 -0400)]
Fix for bug 517.

11 years agoAllow disabling include-file feature
Morgan Deters [Fri, 7 Jun 2013 19:23:36 +0000 (15:23 -0400)]
Allow disabling include-file feature

11 years agosmall parese issue in IDL
Dejan Jovanović [Fri, 7 Jun 2013 02:55:24 +0000 (22:55 -0400)]
small parese issue in IDL

11 years agotypo
Dejan Jovanović [Thu, 6 Jun 2013 19:01:21 +0000 (15:01 -0400)]
typo

11 years agoIDL example theory (to be used with --use-theory=idl).
Dejan Jovanović [Wed, 5 Jun 2013 20:35:37 +0000 (16:35 -0400)]
IDL example theory (to be used with --use-theory=idl).

11 years agoFix bug in --fmf-fmc for producing models of functions not appearing in quantified...
Andrew Reynolds [Wed, 5 Jun 2013 16:23:56 +0000 (11:23 -0500)]
Fix bug in --fmf-fmc for producing models of functions not appearing in quantified formulas.

11 years agoFile inclusion in Smt2 parser.
Morgan Deters [Tue, 4 Jun 2013 19:51:42 +0000 (15:51 -0400)]
File inclusion in Smt2 parser.

The extended command (include-file "filename") now includes file content.

11 years agoAdd --no-condense-function-values option for explicit function models (useful in...
Morgan Deters [Tue, 4 Jun 2013 22:09:48 +0000 (18:09 -0400)]
Add --no-condense-function-values option for explicit function models (useful in some applications)

11 years agoMerge branch '1.2.x'
Morgan Deters [Tue, 4 Jun 2013 23:16:54 +0000 (19:16 -0400)]
Merge branch '1.2.x'

11 years agoFix clang static initialization order issue; fixes bug 512.
Morgan Deters [Tue, 4 Jun 2013 13:10:55 +0000 (09:10 -0400)]
Fix clang static initialization order issue; fixes bug 512.

11 years agoAdd partial support for MBQI with arrays when using --fmf-fmc. Fix constant bounds...
Andrew Reynolds [Tue, 4 Jun 2013 17:12:30 +0000 (12:12 -0500)]
Add partial support for MBQI with arrays when using --fmf-fmc.  Fix constant bounds for bounded integers.

11 years agoMerge tag 'casc24'
Morgan Deters [Mon, 3 Jun 2013 22:03:12 +0000 (18:03 -0400)]
Merge tag 'casc24'

11 years agoUpdated CASC scripts, as provided to Geoff Sutcliffe
Morgan Deters [Mon, 3 Jun 2013 22:02:33 +0000 (18:02 -0400)]
Updated CASC scripts, as provided to Geoff Sutcliffe

11 years agoMerge branch '1.2.x'
Morgan Deters [Wed, 29 May 2013 17:03:03 +0000 (13:03 -0400)]
Merge branch '1.2.x'

11 years agoPer SMT-LIB spec, allow (set-info..) command to succeed implicitly with unknown key.
Morgan Deters [Wed, 29 May 2013 17:02:52 +0000 (13:02 -0400)]
Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with unknown key.

11 years agoSMT-LIB printer updates (some missing cases).
Morgan Deters [Wed, 29 May 2013 13:48:40 +0000 (09:48 -0400)]
SMT-LIB printer updates (some missing cases).

11 years agoFix bug where strict mode didn't allow DIV or MOD, and Ints permitted real division
Morgan Deters [Tue, 28 May 2013 23:06:12 +0000 (19:06 -0400)]
Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real division

11 years agoStandardize SMT-LIBv2 set of logics to use LogicInfo.
Morgan Deters [Tue, 28 May 2013 17:29:59 +0000 (13:29 -0400)]
Standardize SMT-LIBv2 set of logics to use LogicInfo.

Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2.
This led to inconsistencies---such as nonstandard logics like "QF_LIRA"
being accepted in set-logic but not providing the "Real" sort.  Now,
the LogicInfo is used and queried, so nonstandard logics should work
fine and declare the correct symbols.  SMT-LIB v1.2, unfortunately,
can't take advantage of this fully since symbols like "Array" have
substantially different meanings in different logics.

11 years agoRefactoring to prepare for MBQI with integer quantification. Minor bug fixes.
Andrew Reynolds [Thu, 23 May 2013 21:45:47 +0000 (16:45 -0500)]
Refactoring to prepare for MBQI with integer quantification.  Minor bug fixes.

11 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Andrew Reynolds [Wed, 22 May 2013 22:41:11 +0000 (17:41 -0500)]
Merge branch 'master' of https://github.com/CVC4/CVC4

Conflicts:
src/theory/arith/theory_arith_private.cpp
src/theory/quantifiers_engine.cpp

11 years agoSignificant work on bounded integer quantification to handle non-trivial bounds....
Andrew Reynolds [Wed, 22 May 2013 22:34:23 +0000 (17:34 -0500)]
Significant work on bounded integer quantification to handle non-trivial bounds.  Refactoring of InstConstantAttribute to be internal to TermDb.

11 years agoAdd regressions for finite model finding
Andrew Reynolds [Wed, 22 May 2013 21:33:15 +0000 (16:33 -0500)]
Add regressions for finite model finding

11 years agoMerge branch '1.2.x'
Morgan Deters [Tue, 21 May 2013 22:58:32 +0000 (18:58 -0400)]
Merge branch '1.2.x'

11 years agoFix bug 512: an assertion failure only appearing with clang on Mac OS, due to imprope...
Morgan Deters [Tue, 21 May 2013 22:39:33 +0000 (18:39 -0400)]
Fix bug 512: an assertion failure only appearing with clang on Mac OS, due to improper ITE removal in quantifier instantiations.

11 years agoFix an error that valgrind found.
Morgan Deters [Tue, 21 May 2013 22:38:27 +0000 (18:38 -0400)]
Fix an error that valgrind found.

11 years agoMerge branch '1.2.x'
Morgan Deters [Tue, 21 May 2013 20:34:29 +0000 (16:34 -0400)]
Merge branch '1.2.x'

11 years agoFix incremental bug in symmetry breaker.
Morgan Deters [Tue, 21 May 2013 20:18:15 +0000 (16:18 -0400)]
Fix incremental bug in symmetry breaker.

Thanks to Christoph Sticksel for reporting this.

11 years agoMerge branch '1.2.x'
Morgan Deters [Mon, 20 May 2013 23:07:03 +0000 (19:07 -0400)]
Merge branch '1.2.x'

Conflicts:
library_versions
src/parser/parser.h

11 years agoFix error reporting on use of (nonlinear) div,mod,/ symbols
Morgan Deters [Fri, 17 May 2013 20:53:21 +0000 (16:53 -0400)]
Fix error reporting on use of (nonlinear) div,mod,/ symbols

11 years agoUpdate THANKS to mention David Cok's contributions.
Morgan Deters [Fri, 17 May 2013 21:13:36 +0000 (17:13 -0400)]
Update THANKS to mention David Cok's contributions.

11 years agoDetect multiply-defined :named annotations and issue an error.
Morgan Deters [Fri, 17 May 2013 22:14:18 +0000 (18:14 -0400)]
Detect multiply-defined :named annotations and issue an error.

Thanks to David Cok for pointing out this issue.

Conflicts:
library_versions

11 years agoFix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive mode.
Morgan Deters [Fri, 17 May 2013 21:04:34 +0000 (17:04 -0400)]
Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive mode.

Thanks to David Cok for raising this issue.

11 years agoCompliance fixes for :named annotations: they must name closed subterms, the names...
Morgan Deters [Fri, 17 May 2013 16:36:54 +0000 (12:36 -0400)]
Compliance fixes for :named annotations: they must name closed subterms, the names must be user-permitted names, etc.

Thanks to David Cok for raising this issue.

11 years agoDon't allow get-model & co after a user push/pop
Morgan Deters [Fri, 17 May 2013 16:03:29 +0000 (12:03 -0400)]
Don't allow get-model & co after a user push/pop

This makes us more strictly adhere to the spec, but it's useful anyway:
previously we would support a get-model until the problem was explicitly
changed with e.g. a new assertion.  That meant you could check-sat, then
pop, then get-model, but you'd only get the part of the model still in
scope.  This is strange, and would likely lead to problems, so it's now
disabled.

Thanks to David Cok for inquiring about this.

11 years agoAs per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => takes...
Morgan Deters [Fri, 17 May 2013 15:18:12 +0000 (11:18 -0400)]
As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => takes n>2 args and is right-assoc.

Thanks to David Cok for pointing out this issue.

11 years agoFix for equality-chaining of Booleans in SMT-LIBv2.
Morgan Deters [Fri, 17 May 2013 15:12:36 +0000 (11:12 -0400)]
Fix for equality-chaining of Booleans in SMT-LIBv2.

Thanks to David Cok for reporting this.

11 years agoFix destruction issue in GetValueCommand leading to crash.
Morgan Deters [Fri, 17 May 2013 14:38:03 +0000 (10:38 -0400)]
Fix destruction issue in GetValueCommand leading to crash.

Thanks to David Cok for reporting this.

11 years agoBetter error on invalid logic strings.
Morgan Deters [Fri, 17 May 2013 14:19:54 +0000 (10:19 -0400)]
Better error on invalid logic strings.

Thanks to David Cok for reporting this issue.

Conflicts:
library_versions

11 years agoBetter error on illegal (pop N); also more compliant SMT-LIB error messages in some...
Morgan Deters [Fri, 17 May 2013 13:54:15 +0000 (09:54 -0400)]
Better error on illegal (pop N); also more compliant SMT-LIB error messages in some places

Thanks to David Cok for reporting these issues.

11 years agoA couple of fixes to the get-option command for compliance with SMT-LIB.
Morgan Deters [Fri, 17 May 2013 13:27:55 +0000 (09:27 -0400)]
A couple of fixes to the get-option command for compliance with SMT-LIB.

Thanks to David Cok for reporting this issue.

11 years agoDisallow construction of (_ BitVec 0).
Morgan Deters [Fri, 17 May 2013 12:59:25 +0000 (08:59 -0400)]
Disallow construction of (_ BitVec 0).

Thanks to David Cok for reporting this issue.

11 years agoFixed "success" response to (push N) / (pop N) with N > 1.
Morgan Deters [Fri, 17 May 2013 12:51:36 +0000 (08:51 -0400)]
Fixed "success" response to (push N) / (pop N) with N > 1.

Thanks to David Cok for reporting this issue.

11 years agoFix to empty response to (get-assignment).
Morgan Deters [Fri, 17 May 2013 12:43:24 +0000 (08:43 -0400)]
Fix to empty response to (get-assignment).

Thanks to David Cok for reporting this issue.

11 years agoconfigure fix for building with glpk on redhat, perhaps others
Morgan Deters [Thu, 16 May 2013 22:55:08 +0000 (18:55 -0400)]
configure fix for building with glpk on redhat, perhaps others

11 years agominor changes to language bindings
Morgan Deters [Thu, 16 May 2013 21:30:13 +0000 (17:30 -0400)]
minor changes to language bindings

11 years agodisable Logic-checking with finite model finding for now, since FMF uses Rationals...
Morgan Deters [Fri, 10 May 2013 21:08:23 +0000 (17:08 -0400)]
disable Logic-checking with finite model finding for now, since FMF uses Rationals, making the check think arithmetic should be enabled (but it's not)

11 years agoFix erroneous results when the logic was incorrectly specified (by throwing LogicExce...
Morgan Deters [Fri, 10 May 2013 17:01:02 +0000 (13:01 -0400)]
Fix erroneous results when the logic was incorrectly specified (by throwing LogicException).  Also correct a case where sharing was doing some work during pure theory solving.

11 years agoPossible final version of run scripts for casc.
Andrew Reynolds [Mon, 20 May 2013 16:06:02 +0000 (11:06 -0500)]
Possible final version of run scripts for casc.

11 years agoAdd model-producing run script for casc.
Andrew Reynolds [Fri, 17 May 2013 23:17:50 +0000 (18:17 -0500)]
Add model-producing run script for casc.

11 years agoAdd support for --dump-models option, in preparation for casc.
Andrew Reynolds [Fri, 17 May 2013 22:40:34 +0000 (17:40 -0500)]
Add support for --dump-models option, in preparation for casc.

11 years agoAs per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => takes...
Morgan Deters [Fri, 17 May 2013 15:18:12 +0000 (11:18 -0400)]
As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => takes n>2 args and is right-assoc.

Thanks to David Cok for pointing out this issue.

11 years agoFix for equality-chaining of Booleans in SMT-LIBv2.
Morgan Deters [Fri, 17 May 2013 15:12:36 +0000 (11:12 -0400)]
Fix for equality-chaining of Booleans in SMT-LIBv2.

Thanks to David Cok for reporting this.

11 years agoFix destruction issue in GetValueCommand leading to crash.
Morgan Deters [Fri, 17 May 2013 14:38:03 +0000 (10:38 -0400)]
Fix destruction issue in GetValueCommand leading to crash.

Thanks to David Cok for reporting this.

11 years agoBetter error on invalid logic strings.
Morgan Deters [Fri, 17 May 2013 14:19:54 +0000 (10:19 -0400)]
Better error on invalid logic strings.

Thanks to David Cok for reporting this issue.

11 years agoBetter error on illegal (pop N); also more compliant SMT-LIB error messages in some...
Morgan Deters [Fri, 17 May 2013 13:54:15 +0000 (09:54 -0400)]
Better error on illegal (pop N); also more compliant SMT-LIB error messages in some places

Thanks to David Cok for reporting these issues.