cvc5.git
11 years agoFix ECHO command in CVC language parser to not output quotation marks
Morgan Deters [Fri, 15 Feb 2013 16:48:24 +0000 (11:48 -0500)]
Fix ECHO command in CVC language parser to not output quotation marks

11 years agorepairs a bug in rewriterule engine: constructor cannot be used as a pattern
Tianyi Liang [Thu, 14 Feb 2013 05:12:04 +0000 (23:12 -0600)]
repairs a bug in rewriterule engine: constructor cannot be used as a pattern
(cherry picked from commit c33a1abc78bcd51f3f95562b117498caf252cafc)

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
11 years agoRemoving BVDebug and replacing with Debug.
Tim King [Thu, 14 Feb 2013 21:11:42 +0000 (16:11 -0500)]
Removing BVDebug and replacing with Debug.

11 years agoOnly put quantifier assertions in model equality engine if fullModel==true
Morgan Deters [Thu, 7 Feb 2013 21:18:08 +0000 (16:18 -0500)]
Only put quantifier assertions in model equality engine if fullModel==true

11 years agoSignificant work on bug #491 (not yet closed).
Morgan Deters [Fri, 1 Feb 2013 23:00:12 +0000 (18:00 -0500)]
Significant work on bug #491 (not yet closed).

11 years agoMore complete fix for bug 484 (includes fixes for records and tuples).
Morgan Deters [Fri, 21 Dec 2012 23:44:34 +0000 (18:44 -0500)]
More complete fix for bug 484 (includes fixes for records and tuples).

11 years agoFix error in tuple type-checking.
Morgan Deters [Thu, 7 Feb 2013 20:34:23 +0000 (15:34 -0500)]
Fix error in tuple type-checking.

11 years agoMake --default-dag-thresh apply to stringstreams
Morgan Deters [Thu, 7 Feb 2013 20:28:20 +0000 (15:28 -0500)]
Make --default-dag-thresh apply to stringstreams

11 years agoDo not install the "private-library" header
Morgan Deters [Thu, 7 Feb 2013 18:58:22 +0000 (13:58 -0500)]
Do not install the "private-library" header

11 years agomake datatypes enumerator behavior clearer (no exceptions in normal operation)
Morgan Deters [Thu, 7 Feb 2013 02:30:35 +0000 (21:30 -0500)]
make datatypes enumerator behavior clearer (no exceptions in normal operation)

11 years agoFix a compiler warning in NodeBuilder
Morgan Deters [Tue, 5 Feb 2013 21:30:17 +0000 (16:30 -0500)]
Fix a compiler warning in NodeBuilder

11 years agoMerge pull request #3 from kbansal/1.0.x
Kshitij Bansal [Tue, 5 Feb 2013 21:08:13 +0000 (13:08 -0800)]
Merge pull request #3 from kbansal/1.0.x

decision/ : save d_prvsIndex in JH

11 years agodecision/ : save d_prvsIndex in JH
Kshitij Bansal [Wed, 30 Jan 2013 16:59:59 +0000 (11:59 -0500)]
decision/ : save d_prvsIndex in JH

11 years agodos2unix conversion for a number of files; this avoids spurious conflicts when mergin...
Morgan Deters [Tue, 5 Feb 2013 19:28:52 +0000 (14:28 -0500)]
dos2unix conversion for a number of files; this avoids spurious conflicts when merging to master

11 years agoFix NodeBuilder bug which could attempt to allocate beyond hard limit
Morgan Deters [Mon, 4 Feb 2013 23:11:09 +0000 (18:11 -0500)]
Fix NodeBuilder bug which could attempt to allocate beyond hard limit

11 years agodriver::totalTime statistic is now reported correctly on crashes, too
Morgan Deters [Wed, 30 Jan 2013 23:55:44 +0000 (18:55 -0500)]
driver::totalTime statistic is now reported correctly on crashes, too

11 years agoModel no longer adds subterms of quantifiers to equality engine, this fixed bug 492...
Morgan Deters [Mon, 4 Feb 2013 18:52:45 +0000 (13:52 -0500)]
Model no longer adds subterms of quantifiers to equality engine, this fixed bug 492 and resolves previous issue for bug 486.
(cherry picked from *part* of commit e54c0f73712b25f1d6d49a3817c923eea077da81)

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
11 years agoFix a tuple attribute bug that was causing model-generation problems for tuples
Morgan Deters [Fri, 1 Feb 2013 13:31:34 +0000 (08:31 -0500)]
Fix a tuple attribute bug that was causing model-generation problems for tuples

11 years agocorrect output language bug with --dump-to
Morgan Deters [Wed, 30 Jan 2013 20:43:33 +0000 (15:43 -0500)]
correct output language bug with --dump-to

11 years agoFix the regression test for bug 486, and enable it
Morgan Deters [Fri, 25 Jan 2013 20:57:54 +0000 (15:57 -0500)]
Fix the regression test for bug 486, and enable it

(cherry-picked from master 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87)

11 years agomade QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced...
Andrew Reynolds [Mon, 28 Jan 2013 07:57:20 +0000 (01:57 -0600)]
made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent.  this fixes bug 486

(cherry-picked from master c5d1a5d8f898bf22c6bbc98f1d484b07706c035b)

11 years agosome fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory...
Andrew Reynolds [Sun, 27 Jan 2013 17:35:22 +0000 (11:35 -0600)]
some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields

(cherry picked from master bcbf52ffbe0416ecf70bdb644017c338c0540793)

11 years agoanother fix for quantifier models (related to bug 486)
Morgan Deters [Sun, 27 Jan 2013 02:09:55 +0000 (21:09 -0500)]
another fix for quantifier models (related to bug 486)

11 years agofix --check-model --finite-model-find when used together (related to bug 486)
Morgan Deters [Fri, 25 Jan 2013 22:06:02 +0000 (17:06 -0500)]
fix --check-model --finite-model-find when used together (related to bug 486)

11 years agopartially address bug 486: allow some model inspection of quantifiers
Morgan Deters [Wed, 23 Jan 2013 22:00:56 +0000 (17:00 -0500)]
partially address bug 486: allow some model inspection of quantifiers

11 years agoupdate NEWS file
Morgan Deters [Wed, 23 Jan 2013 21:11:55 +0000 (16:11 -0500)]
update NEWS file

11 years agofix for theory preprocessing cache on clang, perhaps others.
Morgan Deters [Tue, 22 Jan 2013 23:03:46 +0000 (18:03 -0500)]
fix for theory preprocessing cache on clang, perhaps others.

11 years agoupdate ANTLR URLs (antlr.org -> antlr3.org)
Morgan Deters [Tue, 22 Jan 2013 17:28:45 +0000 (12:28 -0500)]
update ANTLR URLs (antlr.org -> antlr3.org)

11 years agoFix an options-processing bug on some platforms (e.g., MacOS).
Morgan Deters [Sat, 19 Jan 2013 16:27:03 +0000 (11:27 -0500)]
Fix an options-processing bug on some platforms (e.g., MacOS).

11 years agoadding copy constructor for the datatype enumerator
Dejan Jovanović [Sat, 22 Dec 2012 00:08:26 +0000 (19:08 -0500)]
adding copy constructor for the datatype enumerator
fixes bug 484

11 years agoFix bug 483: readline checks must come after Boost checks in configure
Morgan Deters [Tue, 18 Dec 2012 20:31:45 +0000 (15:31 -0500)]
Fix bug 483: readline checks must come after Boost checks in configure

11 years agoFix printing of EXISTS in CVC language printer
Morgan Deters [Sun, 16 Dec 2012 01:58:31 +0000 (20:58 -0500)]
Fix printing of EXISTS in CVC language printer

11 years agoAdding unit test for different versions of division.
Tim King [Sat, 15 Dec 2012 02:04:41 +0000 (21:04 -0500)]
Adding unit test for different versions of division.

11 years agoMerge remote-tracking branch 'main-repo/1.0.x' into 1.0.x
Tim King [Sat, 15 Dec 2012 01:13:53 +0000 (20:13 -0500)]
Merge remote-tracking branch 'main-repo/1.0.x' into 1.0.x

11 years agoChanging the rewriter to use Boute's Euclidean definition of division.
Tim King [Sat, 15 Dec 2012 01:09:54 +0000 (20:09 -0500)]
Changing the rewriter to use Boute's Euclidean definition of division.

11 years agoMerge pull request #1 from lianah/1.0.x
Dejan Jovanović [Wed, 12 Dec 2012 22:30:09 +0000 (14:30 -0800)]
Merge pull request #1 from lianah/1.0.x

* fixed bug 481 by adding check for division by 0 in bit-vector division...

11 years ago* fixed bug 481 by adding check for division by 0 in bit-vector division circuit
lianah [Wed, 12 Dec 2012 22:26:18 +0000 (17:26 -0500)]
* fixed bug 481 by adding check for division by 0 in bit-vector division circuit
* added printing for total bit-vector division kinds for debugging purposes

11 years agoSMT-LIB compliance fix to get-assignment; resolves bug 480
Morgan Deters [Tue, 11 Dec 2012 23:29:31 +0000 (18:29 -0500)]
SMT-LIB compliance fix to get-assignment; resolves bug 480

11 years agoIgnore unknown term annotations (giving a warning). Resolves bug 479.
Morgan Deters [Tue, 11 Dec 2012 22:55:29 +0000 (17:55 -0500)]
Ignore unknown term annotations (giving a warning).  Resolves bug 479.

11 years agoadding cache for preprocessing datatypes terms to fix bug 475, fix for handling user...
Andrew Reynolds [Tue, 11 Dec 2012 20:47:08 +0000 (14:47 -0600)]
adding cache for preprocessing datatypes terms to fix bug 475, fix for handling user attributes in quantifiers (was broken)

(cherry-picked from commit 206edb6f11674e954f5762a1db9712131151a276)

11 years agoFix bug 476: when CxxTest is not found, make the error less fatal-looking
Morgan Deters [Fri, 7 Dec 2012 22:31:02 +0000 (17:31 -0500)]
Fix bug 476: when CxxTest is not found, make the error less fatal-looking

11 years agoFix to portfolio builds
Morgan Deters [Thu, 6 Dec 2012 23:42:43 +0000 (18:42 -0500)]
Fix to portfolio builds
(cherry picked from commit f46ba71e78054af63b529eb3271952c55beba37e)

11 years agoFix performance issue in a DFS search (bug 474)
Kshitij Bansal [Thu, 6 Dec 2012 21:31:56 +0000 (16:31 -0500)]
Fix performance issue in a DFS search (bug 474)
(cherry picked from commit f056522a587d1b080224992355be070b73d97a3b)

11 years ago* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues
Morgan Deters [Thu, 6 Dec 2012 01:38:17 +0000 (01:38 +0000)]
* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues
* build bugfix for win32
* also fix a bug re: tuples and records in the datatypes rewriter

These fixes are for both trunk and 1.0.x branches.

(cherry picked from commit 8c8985f024cec925f774ff32ebccc306be8e4b26)

11 years agodistribute the find_public_interface.sh script
Morgan Deters [Mon, 3 Dec 2012 22:19:18 +0000 (22:19 +0000)]
distribute the find_public_interface.sh script
(cherry picked from commit af44cd27d5b079f1279c407e610e557e81285d8f)

11 years agoversion numbering
Morgan Deters [Mon, 3 Dec 2012 22:17:04 +0000 (22:17 +0000)]
version numbering
(cherry picked from commit 4cae70d893601a2070dc2b00c5640b48515b1a22)

11 years agoFix for fuzzer-found model bug
Clark Barrett [Mon, 3 Dec 2012 04:35:27 +0000 (04:35 +0000)]
Fix for fuzzer-found model bug

(cherry picked from commit 25c6e1331d338c6ba8d60224711343986e11cf79)

11 years agoCutting release 1.0.
Morgan Deters [Sat, 1 Dec 2012 18:51:31 +0000 (18:51 +0000)]
Cutting release 1.0.

11 years agofix cut-release sanity checks
Morgan Deters [Sat, 1 Dec 2012 17:58:02 +0000 (17:58 +0000)]
fix cut-release sanity checks

11 years agofix to TNode assertion (which is too strict, given lax ordering requirements on stati...
Morgan Deters [Sat, 1 Dec 2012 17:12:18 +0000 (17:12 +0000)]
fix to TNode assertion (which is too strict, given lax ordering requirements on static data initialization)---this should fix debug-staticbinary Mac builds, maybe others

11 years agoThrow a logic exception if user makes an assertion using a STORE_ALL
Clark Barrett [Sat, 1 Dec 2012 16:41:09 +0000 (16:41 +0000)]
Throw a logic exception if user makes an assertion using a STORE_ALL

11 years agoremove instantiator framework
Morgan Deters [Sat, 1 Dec 2012 15:13:58 +0000 (15:13 +0000)]
remove instantiator framework

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agoFix the way abstract values are typed; fixes some compliance issues.
Morgan Deters [Sat, 1 Dec 2012 14:36:14 +0000 (14:36 +0000)]
Fix the way abstract values are typed; fixes some compliance issues.

Also support array-store-all for Boolean terms (related to abstract values, since that's the only way for the user to include an array-store-all in an assertion).

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agofix memory corruption issue in debug builds that led to unhelpful output
Morgan Deters [Sat, 1 Dec 2012 13:47:50 +0000 (13:47 +0000)]
fix memory corruption issue in debug builds that led to unhelpful output

11 years agoremove an obsolete (and incorrect) assertion in boolean-terms; also add failing regre...
Morgan Deters [Sat, 1 Dec 2012 12:42:18 +0000 (12:42 +0000)]
remove an obsolete (and incorrect) assertion in boolean-terms; also add failing regression for bug 472

11 years agofix java system test dependences
Morgan Deters [Sat, 1 Dec 2012 12:18:57 +0000 (12:18 +0000)]
fix java system test dependences

11 years agodrastic simplification of quantifiers code regarding equality queries, instantiation...
Andrew Reynolds [Sat, 1 Dec 2012 02:57:59 +0000 (02:57 +0000)]
drastic simplification of quantifiers code regarding equality queries, instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine

11 years agoFix for a CLN related bug on 32 bit systems. Integer((1<<29)+1) and Integer((long...
Tim King [Sat, 1 Dec 2012 02:09:02 +0000 (02:09 +0000)]
Fix for a CLN related bug on 32 bit systems. Integer((1<<29)+1) and Integer((long int)((1<<29)+1)) gave different values.  This was confirmed on vm-int1.cims.nyu.edu. See ginac.de/CLN/cln_3.html#SEC15 for more details. rational_white and integer_white have tests covering this.

11 years agoSome fixes for boolean arrays
Morgan Deters [Sat, 1 Dec 2012 01:48:40 +0000 (01:48 +0000)]
Some fixes for boolean arrays

also a regression for bug 411

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agofix #line annotation warning
Morgan Deters [Sat, 1 Dec 2012 01:44:07 +0000 (01:44 +0000)]
fix #line annotation warning

11 years agoupdated examples
Morgan Deters [Sat, 1 Dec 2012 01:43:08 +0000 (01:43 +0000)]
updated examples

11 years agoadded a new example for the combination of bit-vectors and arrays (includes model...
Liana Hadarean [Sat, 1 Dec 2012 00:37:22 +0000 (00:37 +0000)]
added a new example for the combination of bit-vectors and arrays (includes model generation) and set the logic for the bitvector example

11 years agoanother part of last commit
Morgan Deters [Sat, 1 Dec 2012 00:33:50 +0000 (00:33 +0000)]
another part of last commit

11 years agodefinition-expansion fixed for get-model, resolves bug 411
Morgan Deters [Sat, 1 Dec 2012 00:31:38 +0000 (00:31 +0000)]
definition-expansion fixed for get-model, resolves bug 411

11 years agoPolishing API examples.
Tim King [Sat, 1 Dec 2012 00:11:20 +0000 (00:11 +0000)]
Polishing API examples.

11 years agoAdding SmtEngine::setLogic(const char* logic) so that smt.setLogic("QF_LRA"); works.
Tim King [Sat, 1 Dec 2012 00:08:38 +0000 (00:08 +0000)]
Adding SmtEngine::setLogic(const char* logic) so that smt.setLogic("QF_LRA"); works.

11 years agoFixes for stricter compilers Andy brought to my attention.
Tim King [Fri, 30 Nov 2012 23:34:47 +0000 (23:34 +0000)]
Fixes for stricter compilers Andy brought to my attention.

11 years agoChanging the documentation of ARR_TABLE_FUN to say (internal symbol).
Tim King [Fri, 30 Nov 2012 23:10:10 +0000 (23:10 +0000)]
Changing the documentation of ARR_TABLE_FUN to say (internal symbol).

11 years agoall API examples now have java versions too; bitvectors gets built; also updated...
Morgan Deters [Fri, 30 Nov 2012 23:07:19 +0000 (23:07 +0000)]
all API examples now have java versions too; bitvectors gets built; also updated old-style copyrights in the examples

11 years agoincorporating some comments from Clark
Morgan Deters [Fri, 30 Nov 2012 23:04:20 +0000 (23:04 +0000)]
incorporating some comments from Clark

11 years agoFix assertion in smt_engine's getValue
Clark Barrett [Fri, 30 Nov 2012 22:44:26 +0000 (22:44 +0000)]
Fix assertion in smt_engine's getValue
Minor changes to RELASE-NOTES

11 years agoUpdating the combination.cpp example.
Tim King [Fri, 30 Nov 2012 22:33:28 +0000 (22:33 +0000)]
Updating the combination.cpp example.

11 years agoCommitting tests to potentially discover an obscure CLN library issue on 32 bit platf...
Tim King [Fri, 30 Nov 2012 22:28:46 +0000 (22:28 +0000)]
Committing tests to potentially discover an obscure CLN library issue on 32 bit platforms. The issue is discussed here: ginac.de/CLN/cln_3.html#SEC15.

11 years agorenaming --smtlib to --smtlib-strict; removing --smtlib2 option
Morgan Deters [Fri, 30 Nov 2012 22:28:06 +0000 (22:28 +0000)]
renaming --smtlib to --smtlib-strict; removing --smtlib2 option

11 years agointernal variables (skolems) aren't printed as part of the model
Morgan Deters [Fri, 30 Nov 2012 21:43:11 +0000 (21:43 +0000)]
internal variables (skolems) aren't printed as part of the model

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agochange detection/handling of output language more reasonably; fixes a nagging bug...
Morgan Deters [Fri, 30 Nov 2012 21:31:12 +0000 (21:31 +0000)]
change detection/handling of output language more reasonably; fixes a nagging bug Tim found in API examples

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agoquantifiers now uses master equality engine, preparation work to cleanup code
Andrew Reynolds [Fri, 30 Nov 2012 20:38:45 +0000 (20:38 +0000)]
quantifiers now uses master equality engine, preparation work to cleanup code

11 years agoparametric datatypes fix related to non-ascribed type constructors introduced by...
Andrew Reynolds [Fri, 30 Nov 2012 20:21:39 +0000 (20:21 +0000)]
parametric datatypes fix related to non-ascribed type constructors introduced by decision procedure

11 years agoadded a simple API example example showing how to use the bit-vector theory.
Liana Hadarean [Fri, 30 Nov 2012 19:44:52 +0000 (19:44 +0000)]
added a simple API example example showing how to use the bit-vector theory.

11 years agoChanges to SExpr to accept autoconversion from bool and const char*. Adding an exampl...
Tim King [Fri, 30 Nov 2012 18:30:37 +0000 (18:30 +0000)]
Changes to SExpr to accept autoconversion from bool and const char*. Adding an example for combination.

11 years agoAdding smtname level options for tlimit, rlimit, etc. Fix to the internal documentati...
Tim King [Fri, 30 Nov 2012 18:16:59 +0000 (18:16 +0000)]
Adding smtname level options for tlimit, rlimit, etc. Fix to the internal documentation in base_options.

11 years agoPartial fix for bug 435; still needs some effort.
Morgan Deters [Fri, 30 Nov 2012 18:11:48 +0000 (18:11 +0000)]
Partial fix for bug 435; still needs some effort.

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agoAdd some regressions for bug 438.
Morgan Deters [Fri, 30 Nov 2012 15:29:36 +0000 (15:29 +0000)]
Add some regressions for bug 438.

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agofix rewrite-rules syntax in regression
Morgan Deters [Fri, 30 Nov 2012 15:14:36 +0000 (15:14 +0000)]
fix rewrite-rules syntax in regression

11 years agominor fix to release script
Morgan Deters [Fri, 30 Nov 2012 14:07:11 +0000 (14:07 +0000)]
minor fix to release script

11 years agofix the syntax of assert-rewrite/-propagation/-reduction by putting the pattern first
François Bobot [Fri, 30 Nov 2012 11:35:02 +0000 (11:35 +0000)]
fix the syntax of assert-rewrite/-propagation/-reduction by putting the pattern first
just after the bindings

 Do it before the release in order to not break user files later

11 years agoreliable benchmark corresponding to bug468
Kshitij Bansal [Thu, 29 Nov 2012 23:55:37 +0000 (23:55 +0000)]
reliable benchmark corresponding to bug468

11 years agorequire type ascriptions for parametric datatype constructors (making them canonical...
Andrew Reynolds [Thu, 29 Nov 2012 23:28:29 +0000 (23:28 +0000)]
require type ascriptions for parametric datatype constructors (making them canonical), this fixes the followup issue of bug 438

11 years agoFix for hidden symbols in library on Mac. It's a strange issue to do with
Morgan Deters [Thu, 29 Nov 2012 23:08:25 +0000 (23:08 +0000)]
Fix for hidden symbols in library on Mac.  It's a strange issue to do with
explicit template instantiation rules, -fvisibility=hidden, and the way that
Apple distributes libstdc++.

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agofixes bug 438, incorporate subtypes into type unification when typechecking parameter...
Andrew Reynolds [Thu, 29 Nov 2012 22:02:20 +0000 (22:02 +0000)]
fixes bug 438, incorporate subtypes into type unification when typechecking parameterized datatypes

11 years agofix for andy: boolean terms stuff really shouldn't look at datatypes at all in this...
Morgan Deters [Thu, 29 Nov 2012 21:34:16 +0000 (21:34 +0000)]
fix for andy: boolean terms stuff really shouldn't look at datatypes at all in this release

11 years agominor documentation fix
Morgan Deters [Thu, 29 Nov 2012 19:37:32 +0000 (19:37 +0000)]
minor documentation fix

11 years agosvn:ignore property
Morgan Deters [Thu, 29 Nov 2012 18:15:56 +0000 (18:15 +0000)]
svn:ignore property

11 years agoFix for nasty corner case found by fuzzer...
Clark Barrett [Thu, 29 Nov 2012 14:28:28 +0000 (14:28 +0000)]
Fix for nasty corner case found by fuzzer...

11 years agoHack to support global variables for CVC language extended to export mechanism.
Kshitij Bansal [Thu, 29 Nov 2012 06:59:21 +0000 (06:59 +0000)]
Hack to support global variables for CVC language extended to export mechanism.
- Adds GlobalVarAttr node attribute

(this commit was certified error- and warning-free by the test-and-commit script.)

11 years agoFixing function models with Boolean terms. Also, LAMBDA's should not be const.
Clark Barrett [Thu, 29 Nov 2012 00:59:06 +0000 (00:59 +0000)]
Fixing function models with Boolean terms.  Also, LAMBDA's should not be const.

11 years agoAdding the helloworld.cpp example.
Tim King [Wed, 28 Nov 2012 22:59:58 +0000 (22:59 +0000)]
Adding the helloworld.cpp example.

11 years agofix a potential race (have failed to reproduce)
Kshitij Bansal [Wed, 28 Nov 2012 21:52:56 +0000 (21:52 +0000)]
fix a potential race (have failed to reproduce)

11 years agoFix for getValue. Now it can handle lambda applications
Clark Barrett [Wed, 28 Nov 2012 21:26:43 +0000 (21:26 +0000)]
Fix for getValue.  Now it can handle lambda applications

11 years agoAttempted "quick-fix" for QF_UF performance regression since Boolean terms added.
Morgan Deters [Wed, 28 Nov 2012 21:18:05 +0000 (21:18 +0000)]
Attempted "quick-fix" for QF_UF performance regression since Boolean terms added.

Sharing is turned on only when Boolean terms are detected during preprocessing.  QF_UF problems (and others)
that don't use any Boolean terms won't have BV turned on.

(this commit was certified error- and warning-free by the test-and-commit script.)